From 5c73b46b58867d4fcf415a4aed961383f32f96e8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Oct 2023 16:49:25 +0200 Subject: [PATCH] Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy The function create_cbv_infos now needs to know if the reduction is expected to be weak or strong. We set it to strong:true, preserving the previous semantics. --- src/covering.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/covering.ml b/src/covering.ml index 1b5474fc..c75da714 100644 --- a/src/covering.ml +++ b/src/covering.ml @@ -887,7 +887,7 @@ let wf_fix_constr env evars sign arity sort carrier cterm crel = in RedFlags.red_add_transparent flags csts in let norm env = - let infos = Cbv.create_cbv_infos reds env !evars in + let infos = Cbv.create_cbv_infos reds ~strong:true env !evars in Cbv.cbv_norm infos in let fixty = norm env fixty in @@ -906,7 +906,7 @@ let wf_fix_constr env evars sign arity sort carrier cterm crel = match kind !evars (whd_all (push_rel_context ctx env) !evars rest) with | Prod (na, b, concl) -> let ctx', rest = Reductionops.whd_decompose_prod_decls (push_rel_context ctx env) !evars b in - let infos = Cbv.create_cbv_infos reds (push_rel_context ctx env) !evars in + let infos = Cbv.create_cbv_infos reds ~strong:true (push_rel_context ctx env) !evars in let norm = Cbv.cbv_norm infos in let fn_type = it_mkProd_or_LetIn rest ctx' in let fn_type = norm fn_type in