diff options
43 files changed, 249 insertions, 250 deletions
diff --git a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh new file mode 100644 index 0000000000..c9ddb3fb9f --- /dev/null +++ b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "11922" ] || [ "$CI_BRANCH" = "rm-local-reductionops" ]; then + + equations_CI_REF="rm-local-reductionops" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + unicoq_CI_REF="rm-local-reductionops" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + +fi diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 9d0552817f..5ad8af6d57 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -187,7 +187,7 @@ let empty_internalization_env = Id.Map.empty let compute_internalization_data env sigma id ty typ impl = let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in - (ty, impl, compute_arguments_scope sigma typ, var_uid id) + (ty, impl, compute_arguments_scope env sigma typ, var_uid id) let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty = List.fold_left3 @@ -2353,9 +2353,9 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty -let scope_of_type_kind sigma = function +let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope sigma typ + | OfType typ -> compute_type_scope env sigma typ | WithoutTypeConstraint | UnknownIfTermOrType -> None let allowed_binder_kind_of_type_kind = function @@ -2372,7 +2372,7 @@ let empty_ltac_sign = { let intern_gen kind env sigma ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = - let tmp_scope = scope_of_type_kind sigma kind in + let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; @@ -2457,7 +2457,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = - let tmp_scope = scope_of_type_kind sigma kind in + let tmp_scope = scope_of_type_kind env sigma kind in let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env diff --git a/interp/notation.ml b/interp/notation.ml index 7761606f11..2703930705 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1448,8 +1448,8 @@ type scope_class = cl_typ let scope_class_compare : scope_class -> scope_class -> int = cl_typ_ord -let compute_scope_class sigma t = - let (cl,_,_) = find_class_type sigma t in +let compute_scope_class env sigma t = + let (cl,_,_) = find_class_type env sigma t in cl module ScopeClassOrd = @@ -1478,22 +1478,23 @@ let find_scope_class_opt = function (**********************************************************************) (* Special scopes associated to arguments of a global reference *) -let rec compute_arguments_classes sigma t = - match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with - | Prod (_,t,u) -> - let cl = try Some (compute_scope_class sigma t) with Not_found -> None in - cl :: compute_arguments_classes sigma u +let rec compute_arguments_classes env sigma t = + match EConstr.kind sigma (Reductionops.whd_betaiotazeta env sigma t) with + | Prod (na, t, u) -> + let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env in + let cl = try Some (compute_scope_class env sigma t) with Not_found -> None in + cl :: compute_arguments_classes env sigma u | _ -> [] -let compute_arguments_scope_full sigma t = - let cls = compute_arguments_classes sigma t in +let compute_arguments_scope_full env sigma t = + let cls = compute_arguments_classes env sigma t in let scs = List.map find_scope_class_opt cls in scs, cls -let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) +let compute_arguments_scope env sigma t = fst (compute_arguments_scope_full env sigma t) -let compute_type_scope sigma t = - find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) +let compute_type_scope env sigma t = + find_scope_class_opt (try Some (compute_scope_class env sigma t) with Not_found -> None) let current_type_scope_name () = find_scope_class_opt (Some CL_SORT) @@ -1531,15 +1532,16 @@ let load_arguments_scope _ (_,(_,r,n,scl,cls)) = let cache_arguments_scope o = load_arguments_scope 1 o -let subst_scope_class subst cs = - try Some (subst_cl_typ subst cs) with Not_found -> None +let subst_scope_class env subst cs = + try Some (subst_cl_typ env subst cs) with Not_found -> None let subst_arguments_scope (subst,(req,r,n,scl,cls)) = let r' = fst (subst_global subst r) in let subst_cl ocl = match ocl with | None -> ocl | Some cl -> - match subst_scope_class subst cl with + let env = Global.env () in + match subst_scope_class env subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in let cls' = List.Smart.map subst_cl cls in @@ -1565,7 +1567,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = | ArgsScopeAuto -> let env = Global.env () in (*FIXME?*) let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in - let scs,cls = compute_arguments_scope_full sigma typ in + let scs,cls = compute_arguments_scope_full env sigma typ in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically @@ -1573,7 +1575,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = of the manually given scopes to avoid further re-computations. *) let env = Global.env () in (*FIXME?*) let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in - let l',cls = compute_arguments_scope_full sigma typ in + let l',cls = compute_arguments_scope_full env sigma typ in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in (req,r,0,l1@l,cls1) @@ -1620,7 +1622,7 @@ let find_arguments_scope r = let declare_ref_arguments_scope sigma ref = let env = Global.env () in (* FIXME? *) let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in - let (scs,cls as o) = compute_arguments_scope_full sigma typ in + let (scs,cls as o) = compute_arguments_scope_full env sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o (********************************) diff --git a/interp/notation.mli b/interp/notation.mli index 842f2b1458..b427aa9bb3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -264,13 +264,13 @@ type scope_class val scope_class_compare : scope_class -> scope_class -> int val subst_scope_class : - Mod_subst.substitution -> scope_class -> scope_class option + Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit -val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list -val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option +val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list +val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index afc83b780b..0f96b9bbe8 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -259,7 +259,7 @@ let parse_ind_args si args relmax = let rec extract_type env sg db j c args = - match EConstr.kind sg (whd_betaiotazeta sg c) with + match EConstr.kind sg (whd_betaiotazeta env sg c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env sg db j d (Array.to_list args' @ args) @@ -380,7 +380,7 @@ and extract_type_app env sg db (r,s) args = and extract_type_scheme env sg db c p = if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta sg c in + let c = whd_betaiotazeta env sg c in match EConstr.kind sg c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 834e4251d3..f13901c36d 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -57,12 +57,12 @@ let make_simple_atoms seq= | None->[] in {negative=seq.latoms;positive=ratoms} -let do_sequent sigma setref triv id seq i dom atoms= +let do_sequent env sigma setref triv id seq i dom atoms= let flag=ref true in let phref=ref triv in let do_atoms a1 a2 = let do_pair t1 t2 = - match unif_atoms sigma i dom t1 t2 with + match unif_atoms env sigma i dom t1 t2 with None->() | Some (Phantom _) ->phref:=true | Some c ->flag:=false;setref:=IS.add (c,id) !setref in @@ -72,16 +72,16 @@ let do_sequent sigma setref triv id seq i dom atoms= do_atoms atoms (make_simple_atoms seq); !flag && !phref -let match_one_quantified_hyp sigma setref seq lf= +let match_one_quantified_hyp env sigma setref seq lf= match lf.pat with Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> - if do_sequent sigma setref triv lf.id seq i dom lf.atoms then + if do_sequent env sigma setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref | _ -> anomaly (Pp.str "can't happen.") -let give_instances sigma lf seq= +let give_instances env sigma lf seq= let setref=ref IS.empty in - List.iter (match_one_quantified_hyp sigma setref seq) lf; + List.iter (match_one_quantified_hyp env sigma setref seq) lf; IS.elements !setref (* collector for the engine *) @@ -129,9 +129,10 @@ let left_instance_tac (inst,id) continue seq= let open EConstr in Proofview.Goal.enter begin fun gl -> let sigma = project gl in + let env = Proofview.Goal.env gl in match inst with Phantom dom-> - if lookup sigma (id,None) seq then + if lookup env sigma (id,None) seq then tclFAIL 0 (Pp.str "already done") else tclTHENS (cut dom) @@ -148,7 +149,7 @@ let left_instance_tac (inst,id) continue seq= tclTRY assumption] | Real((m,t),_)-> let c = (m, EConstr.to_constr sigma t) in - if lookup sigma (id,Some c) seq then + if lookup env sigma (id,Some c) seq then tclFAIL 0 (Pp.str "already done") else let special_generalize= @@ -205,7 +206,8 @@ let instance_tac inst= let quantified_tac lf backtrack continue seq = Proofview.Goal.enter begin fun gl -> - let insts=give_instances (project gl) lf seq in + let env = Proofview.Goal.env gl in + let insts=give_instances env (project gl) lf seq in tclORELSE (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) backtrack diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index c0f4c78ff3..08c2c4d916 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -13,7 +13,7 @@ open Rules val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t -val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> +val give_instances : Environ.env -> Evd.evar_map -> Formula.t list -> Sequent.t -> (Unify.instance * GlobRef.t) list val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7bf13fd25b..3dd5059e5d 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -109,7 +109,7 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup sigma item seq= +let lookup env sigma item seq= History.mem item seq.history || match item with (_,None)->false @@ -117,7 +117,7 @@ let lookup sigma item seq= let p (id2,o)= match o with None -> false - | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in + | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general env sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history let add_formula env sigma side nam t seq = diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 3a5da6ad14..bba89c823c 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -39,7 +39,7 @@ val deepen: t -> t val record: h_item -> t -> t -val lookup: Evd.evar_map -> h_item -> t -> bool +val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index e58e80116d..9c3debe48f 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -29,7 +29,7 @@ let subst_meta subst t = let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t)) -let unif evd t1 t2= +let unif env evd t1 t2= let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -46,8 +46,8 @@ let unif evd t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta evd t1) - and nt2=head_reduce (whd_betaiotazeta evd t2) in + let nt1=head_reduce (whd_betaiotazeta env evd t1) + and nt2=head_reduce (whd_betaiotazeta env evd t2) in match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with Meta i,Meta j-> if not (Int.equal i j) then @@ -123,9 +123,9 @@ let mk_rel_inst evd t= in let nt=renum_rec 0 t in (!new_rel - 1,nt) -let unif_atoms evd i dom t1 t2= +let unif_atoms env evd i dom t1 t2= try - let t=Int.List.assoc i (unif evd t1 t2) in + let t=Int.List.assoc i (unif env evd t1 t2) in if isMeta evd t then Some (Phantom dom) else Some (Real(mk_rel_inst evd t,value evd i t1)) with @@ -136,11 +136,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *) let l=List.init n (fun i->mkMeta (k+i)) in substl l t -let more_general evd (m1,t1) (m2,t2)= +let more_general env evd (m1,t1) (m2,t2)= let mt1=renum_metas_from 0 m1 t1 and mt2=renum_metas_from m1 m2 t2 in try - let sigma=unif evd mt1 mt2 in + let sigma=unif env evd mt1 mt2 in let p (n,t)= n<m1 || isMeta evd t in List.for_all p sigma with UFAIL(_,_)->false diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index 71e786eb90..c6767f04ac 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -13,12 +13,12 @@ open EConstr exception UFAIL of constr*constr -val unif : Evd.evar_map -> constr -> constr -> (int*constr) list +val unif : Environ.env -> Evd.evar_map -> constr -> constr -> (int*constr) list type instance= Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) | Phantom of constr (* domaine de quantification *) -val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option +val unif_atoms : Environ.env -> Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option -val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool +val more_general : Environ.env -> Evd.evar_map -> (int*constr) -> (int*constr) -> bool diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 49fc513dd2..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) = refine to_refine g) ] let find_rectype env sigma c = - let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in + let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in match EConstr.kind sigma t with | Ind ind -> (t, l) | Construct _ -> (t, l) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3b8fb48eb0..d6b2a17882 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite." let rec decompose_app_rel env evd t = (* Head normalize for compatibility with the old meta mechanism *) - let t = Reductionops.whd_betaiota evd t in + let t = Reductionops.whd_betaiota env evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false | App (f, [|arg|]) -> @@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in - let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in + let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in @@ -971,7 +971,7 @@ let unfold_match env sigma sk app = | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in - Reductionops.whd_beta sigma (mkApp (v, args)) + Reductionops.whd_beta env sigma (mkApp (v, args)) | _ -> app let is_rew_cast = function RewCast _ -> true | _ -> false diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e8257b5dba..01e8daf82d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -950,7 +950,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ let open EConstr in if n = 0 then let args = List.rev args in - (if beta then Reductionops.whd_beta sigma else fun x -> x) + (if beta then Reductionops.whd_beta env sigma else fun x -> x) (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma else match kind_of_type sigma ty with | ProdType (_, src, tgt) -> @@ -1065,11 +1065,12 @@ end let introid ?(orig=ref Anonymous) name = let open Proofview.Notations in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let g = Proofview.Goal.concl gl in match EConstr.kind sigma g with | App (hd, _) when EConstr.isLambda sigma hd -> - convert_concl_no_check (Reductionops.whd_beta sigma g) + convert_concl_no_check (Reductionops.whd_beta env sigma g) | _ -> Tacticals.New.tclIDTAC end <*> (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name)) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ab07dd5be9..29a9c65561 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -281,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) = | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) | Proj _ when same_proj sigma0 c t -> body env t c | _ -> - let c = Reductionops.whd_betaiotazeta sigma0 c in + let c = Reductionops.whd_betaiotazeta env sigma0 c in match EConstr.kind sigma0 c with | Const _ when EConstr.eq_constr sigma0 c t -> body env t t | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) @@ -516,7 +516,7 @@ let rwprocess_rule env dir rule = let rec loop d sigma r t0 rs red = let t = if red = 1 then Tacred.hnf_constr env sigma t0 - else Reductionops.whd_betaiotazeta sigma t0 in + else Reductionops.whd_betaiotazeta env sigma t0 in ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index adaf7c8cc1..e004613ef3 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -405,7 +405,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = (* p_origin can be passed to obtain a better error message *) let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let k, f, a = - let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in + let f, a = Reductionops.whd_betaiota_stack env ise (EConstr.of_constr p) in let f = EConstr.Unsafe.to_constr f in let a = List.map EConstr.Unsafe.to_constr a in match kind f with diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fc64022ed4..5e3fb9dae3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1066,7 +1066,7 @@ let adjust_impossible_cases sigma pb pred tomatch submat = (* with .. end *) (* *) (*****************************************************************************) -let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = +let specialize_predicate env newtomatchs (names,depna) arsign cs tms ccl = (* Assume some gamma st: gamma |- PI [X,x:I(X)]. PI tms. ccl *) let nrealargs = List.length names in let l = match depna with Anonymous -> 0 | Name _ -> 1 in @@ -1091,7 +1091,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = (* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *) (* Note: applying the substitution in tms is not important (is it sure?) *) let ccl'' = - whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in + whd_betaiota env Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in (* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *) let ccl''' = liftn_predicate n (n+1) ccl'' tms in (* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*) @@ -1099,7 +1099,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = let find_predicate loc env sigma p current (IndType (indf,realargs)) dep tms = let pred = abstract_predicate env sigma indf current realargs dep tms p in - (pred, whd_betaiota sigma + (pred, whd_betaiota !!env sigma (applist (pred, realargs@[current]))) (* Take into account that a type has been discovered to be inductive, leading @@ -1255,7 +1255,7 @@ let rec generalize_problem names sigma pb = function | LocalDef ({binder_name=Anonymous},_,_) -> pb', deps | _ -> (* for better rendering *) - let d = RelDecl.map_type (fun c -> whd_betaiota sigma c) d in + let d = RelDecl.map_type (fun c -> whd_betaiota !!(pb.env) sigma c) d in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = relocate_index_tomatch sigma (i+1) 1 tomatch in { pb' with @@ -1352,7 +1352,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname) (* Do the specialization for the predicate *) let pred = - specialize_predicate typs' (realnames,curname) arsign const_info tomatch pb.pred in + specialize_predicate !!(pb.env) typs' (realnames,curname) arsign const_info tomatch pb.pred in let currents = List.map (fun x -> Pushed (false,x)) typs' in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 2a844402a8..f931a32bf8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -108,7 +108,7 @@ let app_opt env sigma f t = | None -> sigma, t | Some f -> f sigma t in - sigma, whd_betaiota sigma t + sigma, whd_betaiota env sigma t let pair_of_array a = (a.(0), a.(1)) @@ -130,7 +130,7 @@ let disc_subset sigma x = exception NoSubtacCoercion let hnf env sigma c = whd_all env sigma c -let hnf_nodelta env sigma c = whd_betaiota sigma c +let hnf_nodelta env sigma c = whd_betaiota env sigma c let lift_args n sign = let rec liftrec k = function @@ -343,7 +343,7 @@ let app_coercion env sigma coercion v = | Some f -> let sigma, v' = f sigma v in let sigma, v' = Typing.solve_evars env sigma v' in - sigma, whd_betaiota sigma v' + sigma, whd_betaiota env sigma v' let coerce_itf ?loc env sigma v t c1 = let sigma, coercion = coerce ?loc env sigma t c1 in diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 49401a9937..0c3eaa1da9 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -164,9 +164,9 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *) -let find_class_type sigma t = +let find_class_type env sigma t = let open EConstr in - let t', args = Reductionops.whd_betaiotazeta_stack sigma t in + let t', args = Reductionops.whd_betaiotazeta_stack env sigma t in match EConstr.kind sigma t' with | Var id -> CL_SECVAR id, EInstance.empty, args | Const (sp,u) -> CL_CONST sp, u, args @@ -178,7 +178,7 @@ let find_class_type sigma t = | _ -> raise Not_found -let subst_cl_typ subst ct = match ct with +let subst_cl_typ env subst ct = match ct with CL_SORT | CL_FUN | CL_SECVAR _ -> ct @@ -190,7 +190,7 @@ let subst_cl_typ subst ct = match ct with if c' == c then ct else (match t with | None -> CL_CONST c' | Some t -> - pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value))) + pi1 (find_class_type env Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value))) | CL_IND i -> let i' = subst_ind subst i in if i' == i then ct else CL_IND i' @@ -204,12 +204,12 @@ let subst_coe_typ subst t = subst_global_reference subst t let class_of env sigma t = let (t, n1, i, u, args) = try - let (cl, u, args) = find_class_type sigma t in + let (cl, u, args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) with Not_found -> let t = Tacred.hnf_constr env sigma t in - let (cl, u, args) = find_class_type sigma t in + let (cl, u, args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in (t, n1, i, u, args) in @@ -217,7 +217,7 @@ let class_of env sigma t = let inductive_class_of ind = fst (class_info (CL_IND ind)) -let class_args_of env sigma c = pi3 (find_class_type sigma c) +let class_args_of env sigma c = pi3 (find_class_type env sigma c) let string_of_class = function | CL_FUN -> "Funclass" @@ -249,14 +249,14 @@ let lookup_path_to_sort_from_class s = let apply_on_class_of env sigma t cont = try - let (cl,u,args) = find_class_type sigma t in + let (cl,u,args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; t, cont i with Not_found -> (* Is it worth to be more incremental on the delta steps? *) let t = Tacred.hnf_constr env sigma t in - let (cl, u, args) = find_class_type sigma t in + let (cl, u, args) = find_class_type env sigma t in let (i, { cl_param = n1 } ) = class_info cl in if not (Int.equal (List.length args) n1) then raise Not_found; t, cont i @@ -390,9 +390,10 @@ type coercion = { } let subst_coercion subst c = + let env = Global.env () in let coe = subst_coe_typ subst c.coercion_type in - let cls = subst_cl_typ subst c.coercion_source in - let clt = subst_cl_typ subst c.coercion_target in + let cls = subst_cl_typ env subst c.coercion_source in + let clt = subst_cl_typ env subst c.coercion_target in let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in if c.coercion_type == coe && c.coercion_source == cls && c.coercion_target == clt && c.coercion_is_proj == clp diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 247ef4df75..31600dd17f 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -26,7 +26,7 @@ type cl_typ = (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool -val subst_cl_typ : substitution -> cl_typ -> cl_typ +val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ (** Comparison of [cl_typ] *) val cl_typ_ord : cl_typ -> cl_typ -> int @@ -64,7 +64,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) -val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list +val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_index diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f1506f5f59..36dc01e272 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -136,7 +136,7 @@ let flex_kind_of_term flags env evd c sk = | Cast _ | App _ | Case _ -> assert false let apprec_nohdbeta flags env evd c = - let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in + let (t,sk as appr) = Reductionops.whd_nored_state env evd (c, []) in if flags.modulo_betaiota && Stack.not_purely_applicative sk then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr) @@ -496,8 +496,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 = let term2 = apprec_nohdbeta flags env evd term2 in let default () = evar_eqappr_x flags env evd pbty - (whd_nored_state evd (term1,Stack.empty)) - (whd_nored_state evd (term2,Stack.empty)) + (whd_nored_state env evd (term1,Stack.empty)) + (whd_nored_state env evd (term2,Stack.empty)) in begin match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> @@ -556,7 +556,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env' evd (c'1, Stack.empty) in - let out2, _ = whd_nored_state evd + let out2, _ = whd_nored_state env' evd (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x flags env' evd CONV out1 out2 diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 34684e4a34..348d7c0b2f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -633,7 +633,7 @@ let solve_pattern_eqn env sigma l c = l c in (* Warning: we may miss some opportunity to eta-reduce more since c' is not in normal form *) - shrink_eta c' + shrink_eta env c' (*****************************************) (* Refining/solving unification problems *) @@ -1632,7 +1632,7 @@ let rec invert_definition unify flags choose imitate_defs map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - let rhs = whd_beta evd rhs (* heuristic *) in + let rhs = whd_beta env evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in let names = ref Id.Set.empty in @@ -1758,7 +1758,7 @@ let reconsider_unif_constraints unify flags evd = let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try - let t2 = whd_betaiota evd t2 in (* includes whd_evar *) + let t2 = whd_betaiota env evd t2 in (* includes whd_evar *) let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in reconsider_unif_constraints unify flags evd with diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index b5d81f762a..6132365b27 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -283,9 +283,10 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = in (match optionpos with | None -> + let env' = push_rel d env in mkLambda_name env - (n,t,process_constr (push_rel d env) (i+1) - (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))) + (n,t,process_constr env' (i+1) + (EConstr.Unsafe.to_constr (whd_beta env' Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))) (cprest,rest)) | Some(_,f_0) -> let nF = lift (i+1+decF) f_0 in @@ -293,7 +294,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let arg = process_pos env' nF (lift 1 t) in mkLambda_name env (n,t,process_constr env' (i+1) - (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))) + (EConstr.Unsafe.to_constr (whd_beta env' Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))) (cprest,rest))) | (LocalDef (n,c,t) as d)::cprest, rest -> mkLetIn diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f7e3d651ff..1b6c17fcf9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1025,7 +1025,7 @@ struct | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in - let fsign = Context.Rel.map (whd_betaiota sigma) fsign in + let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in let obj ind rci p v f = @@ -1134,7 +1134,7 @@ struct let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist sigma (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in - let cs_args = Context.Rel.map (whd_betaiota sigma) cs_args in + let cs_args = Context.Rel.map (whd_betaiota !!env sigma) cs_args in let csgn = List.map (set_name Anonymous) cs_args in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f7456ef35e..15bf9667b3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -603,9 +603,7 @@ end (** The type of (machine) states (= lambda-bar-calculus' cuts) *) type state = constr * constr Stack.t -type contextual_reduction_function = env -> evar_map -> constr -> constr -type reduction_function = contextual_reduction_function -type local_reduction_function = evar_map -> constr -> constr +type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = @@ -650,16 +648,6 @@ let strong whdfun env sigma t = map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in strongrec env t -let local_strong whdfun sigma = - let rec strongrec t = EConstr.map sigma strongrec (whdfun sigma t) in - strongrec - -let rec strong_prodspine redfun sigma c = - let x = redfun sigma c in - match EConstr.kind sigma x with - | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b) - | _ -> x - (*************************************) (*** Reduction using bindingss ***) (*************************************) @@ -1225,7 +1213,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res (** reduction machine without global env and refold machinery *) -let local_whd_state_gen flags sigma = +let local_whd_state_gen flags _env sigma = let rec whrec (x, stack) = let c0 = EConstr.kind sigma x in let s = (EConstr.of_kind c0, stack) in @@ -1308,7 +1296,7 @@ let raw_whd_state_gen flags env = f let stack_red_of_state_red f = - let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in + let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in f (* Drops the Cst_stack *) @@ -1319,8 +1307,8 @@ let iterate_whd_gen refold flags env sigma s = Stack.zip sigma ~refold (hd,whd_sk) in aux s -let red_of_state_red f sigma x = - Stack.zip sigma (f sigma (x,Stack.empty)) +let red_of_state_red f env sigma x = + Stack.zip sigma (f env sigma (x,Stack.empty)) (* 0. No Reduction Functions *) @@ -1341,15 +1329,12 @@ let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) let whd_delta_state e = raw_whd_state_gen CClosure.delta e -let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env) -let whd_delta env = red_of_state_red (whd_delta_state env) - -let whd_betadeltazeta_state e = raw_whd_state_gen CClosure.betadeltazeta e -let whd_betadeltazeta_stack env = - stack_red_of_state_red (whd_betadeltazeta_state env) -let whd_betadeltazeta env = - red_of_state_red (whd_betadeltazeta_state env) +let whd_delta_stack = stack_red_of_state_red whd_delta_state +let whd_delta = red_of_state_red whd_delta_state +let whd_betadeltazeta_state = raw_whd_state_gen CClosure.betadeltazeta +let whd_betadeltazeta_stack = stack_red_of_state_red whd_betadeltazeta_state +let whd_betadeltazeta = red_of_state_red whd_betadeltazeta_state (* 3. Iota reduction Functions *) @@ -1361,21 +1346,19 @@ let whd_betaiotazeta_state = local_whd_state_gen CClosure.betaiotazeta let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state -let whd_all_state env = raw_whd_state_gen CClosure.all env -let whd_all_stack env = - stack_red_of_state_red (whd_all_state env) -let whd_all env = - red_of_state_red (whd_all_state env) +let whd_all_state = raw_whd_state_gen CClosure.all +let whd_all_stack = stack_red_of_state_red whd_all_state +let whd_all = red_of_state_red whd_all_state -let whd_allnolet_state env = raw_whd_state_gen CClosure.allnolet env -let whd_allnolet_stack env = - stack_red_of_state_red (whd_allnolet_state env) -let whd_allnolet env = - red_of_state_red (whd_allnolet_state env) +let whd_allnolet_state = raw_whd_state_gen CClosure.allnolet +let whd_allnolet_stack = stack_red_of_state_red whd_allnolet_state +let whd_allnolet = red_of_state_red whd_allnolet_state (* 4. Ad-hoc eta reduction, does not substitute evars *) -let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) +let shrink_eta env c = + let evd = Evd.from_env env in + Stack.zip evd (local_whd_state_gen eta env evd (c,Stack.empty)) (* 5. Zeta Reduction Functions *) @@ -1627,9 +1610,9 @@ let plain_instance sigma s c = empty map). *) -let instance sigma s c = +let instance env sigma s c = (* if s = [] then c else *) - local_strong whd_betaiota sigma (plain_instance sigma s c) + strong whd_betaiota env sigma (plain_instance sigma s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -1795,23 +1778,23 @@ let is_arity env sigma c = (*************************************) (* Metas *) -let meta_value evd mv = +let meta_value env evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> let metas = Metamap.bind valrec b.freemetas in - instance evd metas b.rebus + instance env evd metas b.rebus | None -> mkMeta mv in valrec mv -let meta_instance sigma b = +let meta_instance env sigma b = let fm = b.freemetas in if Metaset.is_empty fm then b.rebus else - let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in - instance sigma c_sigma b.rebus + let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in + instance env sigma c_sigma b.rebus -let nf_meta sigma c = +let nf_meta env sigma c = let cl = mk_freelisted c in - meta_instance sigma { cl with rebus = cl.rebus } + meta_instance env sigma { cl with rebus = cl.rebus } diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 243a2745f0..be91f688e7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -127,9 +127,7 @@ end type state = constr * constr Stack.t -type contextual_reduction_function = env -> evar_map -> constr -> constr -type reduction_function = contextual_reduction_function -type local_reduction_function = evar_map -> constr -> constr +type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -151,8 +149,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) -> (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val local_strong : local_reduction_function -> local_reduction_function -val strong_prodspine : local_reduction_function -> local_reduction_function (*i val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function @@ -181,30 +177,30 @@ val nf_evar : evar_map -> constr -> constr (** Lazy strategy, weak head reduction *) val whd_evar : evar_map -> constr -> constr -val whd_nored : local_reduction_function -val whd_beta : local_reduction_function -val whd_betaiota : local_reduction_function -val whd_betaiotazeta : local_reduction_function -val whd_all : contextual_reduction_function -val whd_allnolet : contextual_reduction_function -val whd_betalet : local_reduction_function +val whd_nored : reduction_function +val whd_beta : reduction_function +val whd_betaiota : reduction_function +val whd_betaiotazeta : reduction_function +val whd_all : reduction_function +val whd_allnolet : reduction_function +val whd_betalet : reduction_function (** Removes cast and put into applicative form *) -val whd_nored_stack : local_stack_reduction_function -val whd_beta_stack : local_stack_reduction_function -val whd_betaiota_stack : local_stack_reduction_function -val whd_betaiotazeta_stack : local_stack_reduction_function +val whd_nored_stack : contextual_stack_reduction_function +val whd_beta_stack : contextual_stack_reduction_function +val whd_betaiota_stack : contextual_stack_reduction_function +val whd_betaiotazeta_stack : contextual_stack_reduction_function val whd_all_stack : contextual_stack_reduction_function val whd_allnolet_stack : contextual_stack_reduction_function -val whd_betalet_stack : local_stack_reduction_function +val whd_betalet_stack : contextual_stack_reduction_function -val whd_nored_state : local_state_reduction_function -val whd_beta_state : local_state_reduction_function -val whd_betaiota_state : local_state_reduction_function -val whd_betaiotazeta_state : local_state_reduction_function +val whd_nored_state : state_reduction_function +val whd_beta_state : state_reduction_function +val whd_betaiota_state : state_reduction_function +val whd_betaiotazeta_state : state_reduction_function val whd_all_state : state_reduction_function val whd_allnolet_state : state_reduction_function -val whd_betalet_state : local_state_reduction_function +val whd_betalet_state : state_reduction_function (** {6 Head normal forms } *) @@ -214,11 +210,11 @@ val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function val whd_betadeltazeta_state : state_reduction_function val whd_betadeltazeta : reduction_function -val whd_zeta_stack : local_stack_reduction_function -val whd_zeta_state : local_state_reduction_function -val whd_zeta : local_reduction_function +val whd_zeta_stack : stack_reduction_function +val whd_zeta_state : state_reduction_function +val whd_zeta : reduction_function -val shrink_eta : constr -> constr +val shrink_eta : Environ.env -> constr -> constr (** Various reduction functions *) @@ -314,5 +310,5 @@ val whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state (** {6 Meta-related reduction functions } *) -val meta_instance : evar_map -> constr freelisted -> constr -val nf_meta : evar_map -> constr -> constr +val meta_instance : env -> evar_map -> constr freelisted -> constr +val nf_meta : env -> evar_map -> constr -> constr diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 1f091c3df8..5ec5005b3e 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -134,7 +134,7 @@ let retype ?(polyprop=true) sigma = let n = inductive_nrealdecls env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with - | Prod _ -> whd_beta sigma (applist (t, [c])) + | Prod _ -> whd_beta env sigma (applist (t, [c])) | _ -> t) | Lambda (name,c1,c2) -> mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2c717b8774..5b9bc91b84 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -252,7 +252,7 @@ let invert_name labs l {binder_name=na0} env sigma ref na = | None -> None | Some c -> let labs',ccl = decompose_lam sigma c in - let _, l' = whd_betalet_stack sigma ccl in + let _, l' = whd_betalet_stack env sigma ccl in let labs' = List.map snd labs' in (* ppedrot: there used to be generic equality on terms here *) let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in @@ -288,7 +288,7 @@ let compute_consteval_direct env sigma ref = let compute_consteval_mutual_fix env sigma ref = let rec srec env minarg labs ref c = - let c',l = whd_betalet_stack sigma c in + let c',l = whd_betalet_stack env sigma c in let nargs = List.length l in match EConstr.kind sigma c' with | Lambda (na,t,g) when List.is_empty l -> @@ -424,7 +424,7 @@ let solve_arity_problem env sigma fxminargs c = let evm = ref sigma in let set_fix i = evm := Evd.define i (mkVar vfx) !evm in let rec check strict c = - let c' = whd_betaiotazeta sigma c in + let c' = whd_betaiotazeta env sigma c in let (h,rcargs) = decompose_app_vect sigma c' in match EConstr.kind sigma h with Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) -> @@ -725,7 +725,7 @@ let rec red_elim_const env sigma ref u largs = if evaluable_reference_eq sigma ref refgoal then (c,args) else - let c', lrest = whd_betalet_stack sigma (applist(c,args)) in + let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in descend (destEvalRefU sigma c') lrest in let (_, midargs as s) = descend (ref,u) largs in let d, lrest = whd_nothing_for_iota env sigma (applist s) in @@ -736,11 +736,11 @@ let rec red_elim_const env sigma ref u largs = | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | NotAnElimination when unfold_nonelim -> let c = reference_value env sigma ref u in - (whd_betaiotazeta sigma (applist (c, largs)), []), nocase + (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase | _ -> raise Redelimination with Redelimination when unfold_anyway -> let c = reference_value env sigma ref u in - (whd_betaiotazeta sigma (applist (c, largs)), []), nocase + (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase and reduce_params env sigma stack l = let len = List.length stack in @@ -849,7 +849,7 @@ and whd_construct_stack env sigma s = let try_red_product env sigma c = let simpfun c = clos_norm_flags betaiotazeta env sigma c in let rec redrec env x = - let x = whd_betaiota sigma x in + let x = whd_betaiota env sigma x in match EConstr.kind sigma x with | App (f,l) -> (match EConstr.kind sigma f with @@ -875,7 +875,7 @@ let try_red_product env sigma c = | _ -> redrec env c in let npars = Projection.npars p in - (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack sigma c') [] with + (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack env sigma c') [] with | Reduced s -> simpfun (applist s) | NotReducible -> raise Redelimination) | _ -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index afd6c33821..d1b65775bd 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -179,7 +179,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = - Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels))) + Reductionops.whd_beta env sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels))) in let instapp = EConstr.Unsafe.to_constr instapp in let projargs = Array.of_list (args @ [instapp]) in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 99a35849e0..f0882d4594 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -29,11 +29,11 @@ open Context.Rel.Declaration module GR = Names.GlobRef -let meta_type evd mv = +let meta_type env evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in - meta_instance evd ty + meta_instance env evd ty let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in @@ -175,7 +175,7 @@ let type_case_branches env sigma (ind,largs) pj c = let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in - let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in + let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in sigma, (lc, ty, Sorts.relevance_of_sort ps) let judge_of_case env sigma ci pj cj lfj = @@ -335,7 +335,7 @@ let rec execute env sigma cstr = let cstr = whd_evar sigma cstr in match EConstr.kind sigma cstr with | Meta n -> - sigma, { uj_val = cstr; uj_type = meta_type sigma n } + sigma, { uj_val = cstr; uj_type = meta_type env sigma n } | Evar ev -> let ty = EConstr.existential_type sigma ev in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 96222f7bf6..5916f0e867 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -35,7 +35,7 @@ val check : env -> evar_map -> constr -> types -> evar_map val type_of_variable : env -> variable -> types (** Returns the instantiated type of a metavariable *) -val meta_type : evar_map -> metavariable -> types +val meta_type : env -> evar_map -> metavariable -> types (** Solve existential variables using typing *) val solve_evars : env -> evar_map -> constr -> evar_map * constr diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f5aaac315a..88eec5ea01 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -708,8 +708,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let stM,stN = extract_instance_status pb in let sigma = if opt.with_types && flags.check_applied_meta_types then - let tyM = Typing.meta_type sigma k1 in - let tyN = Typing.meta_type sigma k2 in + let tyM = Typing.meta_type curenv sigma k1 in + let tyN = Typing.meta_type curenv sigma k2 in let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in check_compatibility curenv CUMUL flags substn l r else sigma @@ -721,7 +721,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let sigma = if opt.with_types && flags.check_applied_meta_types then (try - let tyM = Typing.meta_type sigma k in + let tyM = Typing.meta_type curenv sigma k in let tyN = get_type_of curenv ~lax:true sigma cN in check_compatibility curenv CUMUL flags substn tyN tyM with RetypeError _ -> @@ -742,7 +742,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if opt.with_types && flags.check_applied_meta_types then (try let tyM = get_type_of curenv ~lax:true sigma cM in - let tyN = Typing.meta_type sigma k in + let tyN = Typing.meta_type curenv sigma k in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma) @@ -1040,33 +1040,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> unirec_rec curenvnb pb opt substn - (whd_betaiotazeta sigma (mkApp(c,l1))) cN + (whd_betaiotazeta curenv sigma (mkApp(c,l1))) cN | None -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> unirec_rec curenvnb pb opt substn cM - (whd_betaiotazeta sigma (mkApp(c,l2))) + (whd_betaiotazeta curenv sigma (mkApp(c,l2))) | None -> error_cannot_unify curenv sigma (cM,cN))) | Some false -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> unirec_rec curenvnb pb opt substn cM - (whd_betaiotazeta sigma (mkApp(c,l2))) + (whd_betaiotazeta curenv sigma (mkApp(c,l2))) | None -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> unirec_rec curenvnb pb opt substn - (whd_betaiotazeta sigma (mkApp(c,l1))) cN + (whd_betaiotazeta curenv sigma (mkApp(c,l1))) cN | None -> error_cannot_unify curenv sigma (cM,cN))) and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = if isApp_or_Proj sigma cM then - let f1l1 = whd_nored_state sigma (cM,Stack.empty) in + let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then - let f2l2 = whd_nored_state sigma (cN,Stack.empty) in + let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1080,9 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else try f1 () with e when precatchable_exception e -> if isApp_or_Proj sigma cN then - let f2l2 = whd_nored_state sigma (cN, Stack.empty) in + let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then - let f1l1 = whd_nored_state sigma (cM, Stack.empty) in + let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1306,18 +1306,18 @@ let w_coerce_to_type env evd c cty mvty = let w_coerce env evd mv c = let cty = get_type_of env evd c in - let mvty = Typing.meta_type evd mv in + let mvty = Typing.meta_type env evd mv in w_coerce_to_type env evd c cty mvty let unify_to_type env sigma flags c status u = let sigma, c = refresh_universes (Some false) env sigma c in - let t = get_type_of env sigma (nf_meta sigma c) in - let t = nf_betaiota env sigma (nf_meta sigma t) in + let t = get_type_of env sigma (nf_meta env sigma c) in + let t = nf_betaiota env sigma (nf_meta env sigma t) in unify_0 env sigma CUMUL flags t u let unify_type env sigma flags mv status c = - let mvty = Typing.meta_type sigma mv in - let mvty = nf_meta sigma mvty in + let mvty = Typing.meta_type env sigma mv in + let mvty = nf_meta env sigma mvty in unify_to_type env sigma (set_flags_for_type flags) c status mvty @@ -1476,20 +1476,20 @@ let w_unify_meta_types env ?(flags=default_unify_flags ()) evd = [clenv_typed_unify M N clenv] expects in addition that expected types of metavars are unifiable with the types of their instances *) -let head_app sigma m = - fst (whd_nored_state sigma (m, Stack.empty)) +let head_app env sigma m = + fst (whd_nored_state env sigma (m, Stack.empty)) let isEvar_or_Meta sigma c = match EConstr.kind sigma c with | Evar _ | Meta _ -> true | _ -> false let check_types env flags (sigma,_,_ as subst) m n = - if isEvar_or_Meta sigma (head_app sigma m) then + if isEvar_or_Meta sigma (head_app env sigma m) then unify_0_with_initial_metas subst true env CUMUL flags (get_type_of env sigma n) (get_type_of env sigma m) - else if isEvar_or_Meta sigma (head_app sigma n) then + else if isEvar_or_Meta sigma (head_app env sigma n) then unify_0_with_initial_metas subst true env CUMUL flags (get_type_of env sigma m) @@ -1641,7 +1641,8 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = (fun test -> match test.testing_state with | None -> None | Some (sigma,_,l) -> - let c = applist (local_strong whd_meta sigma c, l) in + let rec strong_whd_meta t = EConstr.map sigma strong_whd_meta (whd_meta sigma t) in + let c = applist (strong_whd_meta c, l) in Some (sigma, c)) let make_eq_test env evd c = @@ -1947,7 +1948,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = (* Remove delta when looking for a subterm *) let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in - let typp = Typing.meta_type evd' p in + let typp = Typing.meta_type env evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in match infer_conv ~pb:CUMUL env evd' predtyp typp with | None -> @@ -1958,7 +1959,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = (evd',[p,pred,(Conv,TypeProcessed)],[]) let secondOrderDependentAbstraction env evd flags typ (p, oplist) = - let typp = Typing.meta_type evd p in + let typp = Typing.meta_type env evd p in let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in w_merge env false flags.merge_unify_flags (evd,[p,pred,(Conv,TypeProcessed)],[]) @@ -1968,8 +1969,8 @@ let secondOrderAbstractionAlgo dep = if dep then secondOrderDependentAbstraction else secondOrderAbstraction let w_unify2 env evd flags dep cv_pb ty1 ty2 = - let c1, oplist1 = whd_nored_stack evd ty1 in - let c2, oplist2 = whd_nored_stack evd ty2 in + let c1, oplist1 = whd_nored_stack env evd ty1 in + let c2, oplist2 = whd_nored_stack env evd ty2 in match EConstr.kind evd c1, EConstr.kind evd c2 with | Meta p1, _ -> (* Find the predicate *) @@ -2000,8 +2001,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 = convertible and first-order otherwise. But if failed if e.g. the type of Meta(1) had meta-variables in it. *) let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = - let hd1,l1 = decompose_app_vect evd (whd_nored evd ty1) in - let hd2,l2 = decompose_app_vect evd (whd_nored evd ty2) in + let hd1,l1 = decompose_app_vect evd (whd_nored env evd ty1) in + let hd2,l2 = decompose_app_vect evd (whd_nored env evd ty2) in let is_empty1 = Array.is_empty l1 in let is_empty2 = Array.is_empty l2 in match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 08178052bf..87b4255b88 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -41,11 +41,11 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = nf_meta clenv.evd c -let clenv_term clenv c = meta_instance clenv.evd c -let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv -let clenv_value clenv = meta_instance clenv.evd clenv.templval -let clenv_type clenv = meta_instance clenv.evd clenv.templtyp +let clenv_nf_meta clenv c = nf_meta clenv.env clenv.evd c +let clenv_term clenv c = meta_instance clenv.env clenv.evd c +let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv +let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval +let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp let refresh_undefined_univs clenv = match EConstr.kind clenv.evd clenv.templval.rebus with @@ -212,19 +212,19 @@ let clenv_assign mv rhs clenv = In any case, we respect the order given in A. *) -let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas +let clenv_metas_in_type_of_meta env evd mv = + (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right - (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.evd mv)) + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv)) mvs Metaset.empty let dependent_closure clenv mvs = let rec aux mvs acc = Metaset.fold (fun mv deps -> - let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) mvs acc in aux mvs mvs @@ -251,7 +251,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce (* Instantiate metas that create beta/iota redexes *) -let meta_reducible_instance evd b = +let meta_reducible_instance env evd b = let fm = b.freemetas in let fold mv accu = let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in @@ -261,7 +261,7 @@ let meta_reducible_instance evd b = in let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = - let u = whd_betaiota Evd.empty u (* FIXME *) in + let u = whd_betaiota env Evd.empty u (* FIXME *) in match EConstr.kind evd u with | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in @@ -314,12 +314,12 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = - if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else clenv_unify CUMUL ~flags - (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv + (meta_reducible_instance clenv.env clenv.evd clenv.templtyp) concl clenv let clenv_unique_resolver ?flags clenv gl = let concl = Proofview.Goal.concl gl in @@ -531,7 +531,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c5e341c720..0257a6f204 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -35,7 +35,7 @@ let clenv_cast_meta clenv = match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with | Meta mv -> (try - let b = Typing.meta_type clenv.evd mv in + let b = Typing.meta_type clenv.env clenv.evd mv in assert (not (occur_meta clenv.evd b)); if occur_meta clenv.evd b then u else mkCast (mkMeta mv, DEFAULTcast, b) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 28b5ed5811..7b323ee0ed 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -485,7 +485,7 @@ let unfold_head env sigma (ids, csts) c = true, EConstr.of_constr (Environ.constant_value_in env (cst, u)) | App (f, args) -> (match aux f with - | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args)) + | true, f' -> true, Reductionops.whd_betaiota env sigma (mkApp (f', args)) | false, _ -> let done_, args' = Array.fold_left_i (fun i (done_, acc) arg -> diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 7c702eab3a..6da2248cc3 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -653,7 +653,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) - (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma + (EConstr.Unsafe.to_constr (Reductionops.whd_beta env sigma (EConstr.of_constr (applist (c, Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' diff --git a/tactics/equality.ml b/tactics/equality.ml index b92a65d767..58345ac253 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -423,7 +423,8 @@ let type_of_clause cls gl = match cls with let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.enter begin fun gl -> let evd = Proofview.Goal.sigma gl in - let isatomic = isProd evd (whd_zeta evd hdcncl) in + let env = Proofview.Goal.env gl in + let isatomic = isProd evd (whd_zeta env evd hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun evd c type_of_cls in @@ -458,7 +459,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in - let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in + let rels, t = decompose_prod_assum sigma (whd_betaiotazeta env sigma ctype) in match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in @@ -475,7 +476,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type env sigma t' with + match match_with_equality_type env' sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -1214,7 +1215,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with + let (a,p_i_minus_1) = match whd_beta_stack env sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in let sigma, ev = Evarutil.new_evar env sigma a in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 76b1c94759..5338e0eef5 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -88,9 +88,9 @@ let is_lax_conjunction = function let prod_assum sigma t = fst (decompose_prod_assum sigma t) (* whd_beta normalize the types of arguments in a product *) -let rec whd_beta_prod sigma c = match EConstr.kind sigma c with - | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c) - | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) +let rec whd_beta_prod env sigma c = match EConstr.kind sigma c with + | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta env sigma t,whd_beta_prod env sigma c) + | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod env sigma c) | _ -> c let match_with_one_constructor env sigma style onlybinary allow_rec t = @@ -119,7 +119,7 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t = else let ctx, cty = mip.mind_nf_lc.(0) in let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - let ctyp = whd_beta_prod sigma + let ctyp = whd_beta_prod env sigma (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c2654486e1..378b6c7418 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1319,7 +1319,7 @@ let cut c = let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) - let c = if normalize_cut then local_strong whd_betaiota sigma c else c in + let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in @@ -1607,7 +1607,7 @@ let make_projection env sigma params cstr sign elim i n c u = noccur_between sigma 1 (n-i-1) t (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) - && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) + && not (isEvar sigma (fst (whd_betaiota_stack env sigma t))) && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) then let t = lift (i+1-n) t in @@ -3025,7 +3025,7 @@ let specialize (c,lbind) ipat = let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let sigma = clause.evd in - let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in + let (thd,tstack) = whd_nored_stack env sigma (clenv_value clause) in (* The completely applied term is (thd tstack), but tstack may contain unsolved metas, so now we must reabstract them args with there name to have diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 743d1d2026..5323c9f1c6 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -139,7 +139,7 @@ let build_beq_scheme_deps kn = perfomed in a much cleaner way, e.g. using the kernel normal form of constructor types and kernel whd_all for the argument types. *) let rec aux accu c = - let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in + let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in match Constr.kind c with | Cast (x,_,_) -> aux accu (Term.applist (x,a)) @@ -238,7 +238,7 @@ let build_beq_scheme mode kn = let compute_A_equality rel_list nlist eqA ndx t = let lifti = ndx in let rec aux c = - let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in + let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in match Constr.kind c with | Rel x -> mkRel (x-nlist+ndx) diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index d6be02245c..3cc5dd65af 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -111,7 +111,7 @@ la liste des variables dont depend la classe source l'indice de la classe source dans la liste lp *) -let get_source lp source = +let get_source env lp source = let open Context.Rel.Declaration in match source with | None -> @@ -120,7 +120,7 @@ let get_source lp source = | [] -> raise Not_found | LocalDef _ :: lt -> aux lt | LocalAssum (_,t1) :: lt -> - let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in cl1,lt,lv1,1 in aux lp | Some cl -> @@ -130,17 +130,17 @@ let get_source lp source = | LocalDef _ as decl :: lt -> aux (decl::acc) lt | LocalAssum (_,t1) as decl :: lt -> try - let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in + let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1 else raise Not_found with Not_found -> aux (decl::acc) lt in aux [] (List.rev lp) -let get_target t ind = +let get_target env t ind = if (ind > 1) then CL_FUN else - match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with + match pi1 (find_class_type env Evd.empty (EConstr.of_constr t)) with | CL_CONST p when Recordops.is_primitive_projection p -> CL_PROJ (Option.get @@ Recordops.find_primitive_projection p) | x -> x @@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly = match idf_opt with | Some idf -> idf | None -> - let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in + let cl,u,_ = find_class_type env sigma (EConstr.of_constr t) in Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in @@ -298,14 +298,15 @@ let warn_uniform_inheritance = let add_new_coercion_core coef stre poly source target isid = check_source source; - let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in + let env = Global.env () in + let t, _ = Typeops.type_of_global_in_context env coef in if coercion_exists coef then raise (CoercionError AlreadyExists); let lp,tg = decompose_prod_assum t in let llp = List.length lp in if Int.equal llp 0 then raise (CoercionError NotAFunction); let (cls,ctx,lvs,ind) = try - get_source lp source + get_source env lp source with Not_found -> raise (CoercionError (NoSource source)) in @@ -315,7 +316,7 @@ let add_new_coercion_core coef stre poly source target isid = warn_uniform_inheritance coef; let clt = try - get_target tg ind + get_target env tg ind with Not_found -> raise (CoercionError NoTarget) in diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 2fd6fe2b29..ec37ec7fa8 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -33,7 +33,7 @@ let project_hint ~poly pri l2r r = let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in let sigma, p = Evd.fresh_global env sigma p in let c = - Reductionops.whd_beta sigma + Reductionops.whd_beta env sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 32affd562f..8435612abd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1757,7 +1757,8 @@ let cache_scope_command o = let subst_scope_command (subst,(local,scope,o as x)) = match o with | ScopeClasses cl -> - let cl' = List.map_filter (subst_scope_class subst) cl in + let env = Global.env () in + let cl' = List.map_filter (subst_scope_class env subst) cl in let cl' = if List.for_all2eq (==) cl cl' then cl else cl' in |