Skip to content

Commit

Permalink
Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
herbelin committed Nov 15, 2023
1 parent d913185 commit 5c73b46
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/covering.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit 5c73b46

Please sign in to comment.