diff options
| author | Pierre-Marie Pédrot | 2018-10-31 13:10:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-31 13:10:25 +0100 |
| commit | ec73ad521123e11ad8e1c6c916de48ae30b12639 (patch) | |
| tree | 00674110236525a6217e33a88b7e94af4ce00ad9 /plugins/funind/functional_principles_proofs.ml | |
| parent | e29dc5ab5e85eb5f740de83f9f0b97b233651a3e (diff) | |
| parent | 6c4e4b9fc63b3282422024d556a644adc55b13f6 (diff) | |
Merge PR #8864: Avoid passing empty environments
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ad1114b733..d4e410bd69 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -229,10 +229,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t = true with Not_found -> false -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env - - exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = @@ -420,7 +416,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in - let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in + let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp @@ -800,7 +796,7 @@ let build_proof g | LetIn _ -> let new_infos = - { dyn_infos with info = nf_betaiotazeta dyn_infos.info } + { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in tclTHENLIST @@ -834,7 +830,7 @@ let build_proof | LetIn _ -> let new_infos = { dyn_infos with - info = nf_betaiotazeta dyn_infos.info + info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in @@ -977,7 +973,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "body " ++ pr_lconstr bodies.(num)); *) let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) - let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in + let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f |