Skip to content

Commit

Permalink
Merge pull request #566 from herbelin/master+adapt-coq-pr18190-whd-cbv
Browse files Browse the repository at this point in the history
Adapt to coq PR #18190 adding a whd form of the cbv reduction strategy
  • Loading branch information
ppedrot authored Nov 21, 2023

Verified

This commit was signed with the committer’s verified signature. The key has expired.
ulyssa Ulyssa
2 parents d913185 + 5c73b46 commit 79d3a45
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
@@ -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

0 comments on commit 79d3a45

Please sign in to comment.