From e6353e9ef6542b444391a46d9557ebf3a6443947 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Feb 2018 15:55:54 +0100 Subject: Reductionops.nf_* now take an environment. --- plugins/funind/functional_principles_proofs.ml | 15 ++++++++------- plugins/ltac/rewrite.ml | 13 ++++++------- plugins/omega/coq_omega.ml | 2 +- plugins/ssr/ssrcommon.ml | 4 ++-- 4 files changed, 17 insertions(+), 17 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 62ca70626..d04887a48 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -324,7 +324,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = context in let new_type_of_hyp = - Reductionops.nf_betaiota sigma new_type_of_hyp in + Reductionops.nf_betaiota env sigma new_type_of_hyp in let new_ctxt,new_end_of_type = decompose_prod_n_assum sigma ctxt_size new_type_of_hyp in @@ -698,6 +698,7 @@ let build_proof : tactic = let rec build_proof_aux do_finalize dyn_infos : tactic = fun g -> + let env = pf_env g in let sigma = project g in (* observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*) match EConstr.kind sigma dyn_infos.info with @@ -794,7 +795,7 @@ let build_proof do_finalize dyn_infos g | Lambda _ -> let new_term = - Reductionops.nf_beta sigma dyn_infos.info in + Reductionops.nf_beta env sigma dyn_infos.info in build_proof do_finalize {dyn_infos with info = new_term} g | LetIn _ -> @@ -1153,7 +1154,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let bodies_with_all_params = Array.map (fun body -> - Reductionops.nf_betaiota (project g) + Reductionops.nf_betaiota (pf_env g) (project g) (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body, List.rev_map var_of_decl princ_params)) ) @@ -1191,12 +1192,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let body_with_param,num = let body = get_body fnames.(i) in let body_with_full_params = - Reductionops.nf_betaiota (project g) ( + Reductionops.nf_betaiota (pf_env g) (project g) ( applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with | Fix((_,num),(_,_,bs)) -> - Reductionops.nf_betaiota (project g) + Reductionops.nf_betaiota (pf_env g) (project g) ( (applist (substl @@ -1279,7 +1280,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota (project g) + Reductionops.nf_betaiota (pf_env g) (project g) (applist(fix_body,List.rev_map mkVar args_id)); eq_hyps = [] } @@ -1339,7 +1340,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota Evd.empty + Reductionops.nf_betaiota (pf_env g) Evd.empty (applist(fbody_with_full_params, (List.rev_map var_of_decl princ_params)@ (List.rev_map mkVar args_id) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3cbb11001..acd7a30c4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -210,9 +210,9 @@ end) = struct let t = Reductionops.whd_all env (goalevars evars) ty in match EConstr.kind (goalevars evars) t, l with | Prod (na, ty, b), obj :: cstrs -> - let b = Reductionops.nf_betaiota (goalevars evars) b in + let b = Reductionops.nf_betaiota env (goalevars evars) b in if noccurn (goalevars evars) 1 b (* non-dependent product *) then - let ty = Reductionops.nf_betaiota (goalevars evars) ty in + let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in let evars, relty = mk_relty evars env ty obj in let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in @@ -221,7 +221,7 @@ end) = struct let (evars, b, arg, cstrs) = aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs in - let ty = Reductionops.nf_betaiota (goalevars evars) ty in + let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let pred = mkLambda (na, ty, b) in let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in @@ -231,7 +231,7 @@ end) = struct | _, [] -> (match finalcstr with | None | Some (_, None) -> - let t = Reductionops.nf_betaiota (fst evars) ty in + let t = Reductionops.nf_betaiota env (fst evars) ty in let evars, rel = mk_relty evars env t None in evars, t, rel, [t, Some rel] | Some (t, Some rel) -> evars, t, rel, [t, Some rel]) @@ -1557,9 +1557,8 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in (** For compatibility *) - let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in - let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in + let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in + let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 869284246..4271c80cd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -652,7 +652,7 @@ let decompile af = (** Backward compat to emulate the old Refine: normalize the goal conclusion *) let new_hole env sigma c = - let c = Reductionops.nf_betaiota sigma c in + let c = Reductionops.nf_betaiota env sigma c in Evarutil.new_evar env sigma c let clever_rewrite_base_poly typ p result theorem = diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 8493dbdbb..7cdf05117 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = | _ -> Constr.fold put evlist c in let evlist = put [] c0 in if evlist = [] then 0, c0 else - let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in + let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") (fun (k,_) -> Evar.print k) evlist)); let evplist = @@ -894,7 +894,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ let sigma = create_evar_defs sigma in let (sigma, x) = Evarutil.new_evar env sigma - (if bi_types then Reductionops.nf_betaiota sigma src else src) in + (if bi_types then Reductionops.nf_betaiota env sigma src else src) in loop (EConstr.Vars.subst1 x tgt) ((m - n,x) :: args) sigma (n-1) | CastType (t, _) -> loop t args sigma n | LetInType (_, v, _, t) -> loop (EConstr.Vars.subst1 v t) args sigma n -- cgit v1.2.3