diff options
65 files changed, 343 insertions, 344 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 9c05c6c02..6380e3fc1 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -729,13 +729,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = (* excluding defined evars *) -let evar_list c = - let rec evrec acc c = - match kind_of_term c with - | Evar (evk, _ as ev) -> ev :: acc - | _ -> Term.fold_constr evrec acc c in - evrec [] c - let evars_of_term c = let rec evrec acc c = match kind_of_term c with diff --git a/engine/evd.mli b/engine/evd.mli index 4e8284675..699b52c2b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -420,10 +420,6 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t contained in the object; need the term to be evar-normal otherwise defined evars are returned too. *) -val evar_list : constr -> existential list - (** excluding evars in instances of evars and collected with - redundancies from right to left (used by tactic "instantiate") *) - val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d4d87f2a..e5dd6a6ec 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1982,7 +1982,7 @@ let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = - interp_gen (OfType (EConstr.of_constr typ)) env sigma ~impls c + interp_gen (OfType typ) env sigma ~impls c (* Not all evars expected to be resolved *) @@ -2001,7 +2001,7 @@ let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c + interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls IsType c @@ -2093,6 +2093,7 @@ let interp_rawcontext_evars env evdref k bl = let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> + let t = EConstr.Unsafe.to_constr t in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2102,7 +2103,9 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let t = EConstr.Unsafe.to_constr t in + let c = EConstr.Unsafe.to_constr c in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 61e7c6f5c..2f6795ed4 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -101,7 +101,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> - constr_expr -> types -> constr Evd.in_evar_universe_context + constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context @@ -109,32 +109,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr (** Accepting unresolved evars *) val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> constr + ?impls:internalization_env -> constr_expr -> EConstr.constr val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> constr + ?impls:internalization_env -> constr_expr -> types -> EConstr.constr val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types + ?impls:internalization_env -> constr_expr -> EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) val interp_constr_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - constr * Impargs.manual_implicits + EConstr.constr * Impargs.manual_implicits val interp_casted_constr_evars_impls : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> - constr * Impargs.manual_implicits + ?impls:internalization_env -> constr_expr -> EConstr.types -> + EConstr.constr * Impargs.manual_implicits val interp_type_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - types * Impargs.manual_implicits + EConstr.types * Impargs.manual_implicits (** Interprets constr patterns *) @@ -153,7 +153,7 @@ val interp_reference : ltac_sign -> reference -> glob_constr val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types +val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types (** Interpret contexts: returns extended env and context *) diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 6b94da28a..01cff94a8 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -7,6 +7,9 @@ (************************************************************************) open Util +open Names +open Term +open EConstr open CErrors open Evar_refiner open Tacmach @@ -35,25 +38,32 @@ let instantiate_evar evk (ist,rawc) sigma = let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in tclEVARS sigma' +let evar_list sigma c = + let rec evrec acc c = + match EConstr.kind sigma c with + | Evar (evk, _ as ev) -> ev :: acc + | _ -> EConstr.fold sigma evrec acc c in + evrec [] c + let instantiate_tac n c ido = Proofview.V82.tactic begin fun gl -> let sigma = gl.sigma in let evl = match ido with - ConclLocation () -> evar_list (pf_concl gl) + ConclLocation () -> evar_list sigma (pf_concl gl) | HypLocation (id,hloc) -> let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in match hloc with InHyp -> (match decl with - | LocalAssum (_,typ) -> evar_list typ + | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ) | _ -> error "Please be more specific: in type or value?") | InHypTypeOnly -> - evar_list (NamedDecl.get_type decl) + evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl)) | InHypValueOnly -> (match decl with - | LocalDef (_,body,_) -> evar_list body + | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body) | _ -> error "Not a defined hypothesis.") in if List.length evl < n then error "Not enough uninstantiated existential variables."; @@ -92,3 +102,18 @@ let let_evar name typ = in Sigma (tac, sigma, p) end } + +let hget_evar n = + let open EConstr in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let evl = evar_list sigma concl in + if List.length evl < n then + error "Not enough uninstantiated existential variables."; + if n <= 0 then error "Incorrect existential variable index."; + let ev = List.nth evl (n-1) in + let ev_type = EConstr.existential_type sigma ev in + Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) + end } + diff --git a/ltac/evar_tactics.mli b/ltac/evar_tactics.mli index 41266e61c..cfe747665 100644 --- a/ltac/evar_tactics.mli +++ b/ltac/evar_tactics.mli @@ -17,3 +17,5 @@ val instantiate_tac_by_name : Id.t -> Tacinterp.interp_sign * Glob_term.glob_constr -> unit Proofview.tactic val let_evar : Name.t -> EConstr.types -> unit Proofview.tactic + +val hget_evar : int -> unit Proofview.tactic diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index f8db0b4fc..53b726432 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -177,7 +177,7 @@ ARGUMENT EXTEND lglob END let interp_casted_constr ist gl c = - interp_constr_gen (Pretyping.OfType (EConstr.of_constr (pf_concl gl))) ist (pf_env gl) (project gl) c + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c ARGUMENT EXTEND casted_constr TYPED AS constr diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 65c75703b..519633bbe 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -693,24 +693,8 @@ END hget_evar *) -let hget_evar n = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let sigma = Tacmach.New.project gl in - let concl = Proofview.Goal.concl gl in - let concl = EConstr.Unsafe.to_constr concl in - let evl = evar_list concl in - let concl = EConstr.of_constr concl in - if List.length evl < n then - error "Not enough uninstantiated existential variables."; - if n <= 0 then error "Incorrect existential variable index."; - let ev = List.nth evl (n-1) in - let ev = (fst ev, Array.map EConstr.of_constr (snd ev)) in - let ev_type = existential_type sigma ev in - change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) - end } - TACTIC EXTEND hget_evar -| [ "hget_evar" int_or_var(n) ] -> [ hget_evar n ] +| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ] END (**********************************************************************) @@ -747,7 +731,6 @@ let refl_equal = let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in - let type_of_a = EConstr.of_constr type_of_a in Tacticals.New.tclTHENLIST [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; Proofview.Goal.nf_enter { enter = begin fun gl -> @@ -804,7 +787,6 @@ let destauto t = let destauto_in id = Proofview.Goal.nf_enter { enter = begin fun gl -> let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in - let ctype = EConstr.of_constr ctype in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype @@ -1088,7 +1070,7 @@ END VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF | [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ - let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in + let it c = EConstr.Unsafe.to_constr (snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c)) in let k1 = Keys.constr_key (it c) in let k2 = Keys.constr_key (it c') in match k1, k2 with diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 3c6bd4563..715929c56 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -135,7 +135,6 @@ let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in let evdref = ref evars in let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in - let t = EConstr.of_constr t in (!evdref, cstrs), t let app_poly_nocheck env evars f args = @@ -509,7 +508,6 @@ let rec decompose_app_rel env evd t = | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in let ty = Typing.unsafe_type_of env evd argl in - let ty = EConstr.of_constr ty in let f'' = mkLambda (Name default_dependent_ident, ty, mkLambda (Name (Id.of_string "y"), lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) @@ -813,7 +811,6 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in - let appmtype = EConstr.of_constr appmtype in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1445,7 +1442,6 @@ module Strategies = fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> (* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in - let c = EConstr.of_constr c in let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> @@ -1693,7 +1689,6 @@ let cl_rewrite_clause_strat strat clause = let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) -> let c sigma = let (sigma, c) = Pretyping.understand_tcc env sigma c in - let c = EConstr.of_constr c in (sigma, (c, NoBindings)) in let flags = general_rewrite_unif_flags () in @@ -1702,7 +1697,6 @@ let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) let interp_glob_constr_list env = let make c = (); fun sigma -> let sigma, c = Pretyping.understand_tcc env sigma c in - let c = EConstr.of_constr c in (sigma, (c, NoBindings)) in List.map (fun c -> make c, true, None) @@ -1940,7 +1934,6 @@ let build_morphism_signature env sigma m = let m = EConstr.of_constr m in let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in - let t = EConstr.of_constr t in let cstrs = let rec aux t = match EConstr.kind sigma t with @@ -1971,7 +1964,6 @@ let default_morphism sign m = let env = Global.env () in let sigma = Evd.from_env env in let t = Typing.unsafe_type_of env sigma m in - let t = EConstr.of_constr t in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -2111,7 +2103,7 @@ let get_hyp gl (c,l) clause l2r = let env = Tacmach.New.pf_env gl in let sigma, hi = decompose_applied_relation env evars (c,l) in let but = match clause with - | Some id -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl) + | Some id -> Tacmach.New.pf_get_hyp_typ id gl | None -> nf_evar evars (Tacmach.New.pf_concl gl) in unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env @@ -2228,7 +2220,6 @@ let setoid_symmetry_in id = Proofview.V82.tactic (fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in - let ctype = EConstr.of_constr ctype in let binders,concl = decompose_prod_assum sigma ctype in let (equiv, args) = decompose_app sigma concl in let rec split_last_two = function diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index d8df07733..36a0336bc 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -636,7 +636,6 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) c in - let c = EConstr.of_constr c in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) @@ -795,7 +794,6 @@ let interp_may_eval f ist env sigma = function let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in - let c = EConstr.of_constr c in !evdref , c with | Not_found -> diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 0a980c03b..aedcb7575 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -452,8 +452,9 @@ and applist_projection c l = applistc (mkProj (p, hd)) tl) | _ -> applistc c l -let rec canonize_name c = - let func = canonize_name in +let rec canonize_name sigma c = + let c = EConstr.Unsafe.to_constr c in + let func c = canonize_name sigma (EConstr.of_constr c) in match kind_of_term c with | Const (kn,u) -> let canon_const = constant_of_kn (canonical_con kn) in @@ -509,7 +510,7 @@ let rec add_term state t= let b=next uf in let trm = constr_of_term t in let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in - let typ = canonize_name typ in + let typ = canonize_name (project state.gls) typ in let new_node= match t with Symb _ | Product (_,_) -> @@ -833,6 +834,7 @@ let complete_one_class state i= app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in let _c = pf_unsafe_type_of state.gls (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in + let _c = EConstr.Unsafe.to_constr _c in let _args = List.map (fun i -> constr_of_term (term state.uf i)) pac.args in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 62892973d..2ab4dced4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -219,7 +219,7 @@ let make_prb gls depth additionnal_terms = | `Nrule patts -> add_quant state id false patts end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it)); begin - match atom_of_constr env sigma (EConstr.of_constr (pf_concl gls)) with + match atom_of_constr env sigma (pf_concl gls) with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter @@ -271,7 +271,7 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> - let type_of t = EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t) in + let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) @@ -343,7 +343,7 @@ let refute_tac c t1 t2 p = let neweq= new_app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt1)) k + in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k end } let refine_exact_check c gl = @@ -361,7 +361,7 @@ let convert_to_goal_tac c t1 t2 p = let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] - in refresh_universes (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl tt2)) k + in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end } let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p = let trivial = Universes.constr_of_global (Lazy.force _True) in let trivial = EConstr.of_constr trivial in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in + let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in let pred = mkLambda(Name xid,outtype,mkRel 1) in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 7123ebcaf..6a0ec3968 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -74,7 +74,7 @@ let tcl_change_info_gen info_gen = let concl = pf_concl gls in let hyps = Goal.V82.hyps (project gls) it in let extra = Goal.V82.extra (project gls) it in - let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps (EConstr.of_constr concl) (info_gen extra) in + let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in let sigma = Goal.V82.partial_solution sigma it ev in { it = [gl] ; sigma= sigma; } ) @@ -88,7 +88,7 @@ let tcl_erase_info gls = let special_whd gl= let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in - (fun t -> CClosure.whd_val infos (CClosure.inject t)) + (fun t -> CClosure.whd_val infos (CClosure.inject (EConstr.Unsafe.to_constr t))) let special_nf gl= let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in @@ -342,7 +342,7 @@ let rec replace_in_list m l = function | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q let enstack_subsubgoals env se stack gls= - let hd,params = decompose_app (special_whd gls se.se_type) in + let hd,params = decompose_app (special_whd gls (EConstr.of_constr se.se_type)) in match kind_of_term hd with Ind (ind,u as indu) when is_good_inductive env ind -> (* MS: FIXME *) let mib,oib= @@ -397,6 +397,7 @@ let rec nf_list evd = let find_subsubgoal c ctyp skip submetas gls = let env= pf_env gls in let concl = pf_concl gls in + let concl = EConstr.Unsafe.to_constr concl in let evd = mk_evd ((0,concl)::submetas) gls in let stack = Stack.create () in let max_meta = @@ -412,7 +413,7 @@ let find_subsubgoal c ctyp skip submetas gls = try let unifier = Unification.w_unify env se.se_evd Reduction.CUMUL - ~flags:(Unification.elim_flags ()) (EConstr.of_constr ctyp) (EConstr.of_constr se.se_type) in + ~flags:(Unification.elim_flags ()) ctyp (EConstr.of_constr se.se_type) in if n <= 0 then {se with se_evd=meta_assign se.se_meta @@ -433,7 +434,8 @@ let concl_refiner metas body gls = let concl = pf_concl gls in let evd = sig_sig gls in let env = pf_env gls in - let sort = family_of_sort (Typing.e_sort_of env (ref evd) (EConstr.of_constr concl)) in + let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in + let concl = EConstr.Unsafe.to_constr concl in let rec aux env avoid subst = function [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> @@ -504,7 +506,7 @@ let mk_stat_or_thesis info gls = function This c -> c | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." - | Thesis Plain -> pf_concl gls + | Thesis Plain -> EConstr.Unsafe.to_constr (pf_concl gls) let just_tac _then cut info gls0 = let last_item = @@ -536,7 +538,7 @@ let instr_cut mkstat _thus _then cut gls0 = let c_stat = mkstat info gls0 stat.st_it in let thus_tac gls= if _thus then - thus_tac (mkVar c_id) c_stat [] gls + thus_tac (mkVar c_id) (EConstr.of_constr c_stat) [] gls else tclIDTAC gls in tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat)) [tclTHEN tcl_erase_info (just_tac _then cut info); @@ -582,7 +584,7 @@ let instr_rew _thus rew_side cut gls0 = | Name id -> id,true in let thus_tac new_eq gls= if _thus then - thus_tac (mkVar c_id) new_eq [] gls + thus_tac (mkVar c_id) (EConstr.of_constr new_eq) [] gls else tclIDTAC gls in match rew_side with Lhs -> @@ -610,7 +612,7 @@ let instr_claim _thus st gls0 = | Name id -> id,true in let thus_tac gls= if _thus then - thus_tac (mkVar id) st.st_it [] gls + thus_tac (mkVar id) (EConstr.of_constr st.st_it) [] gls else tclIDTAC gls in let ninfo1 = {pm_stack= (if _thus then Focus_claim else Claim)::info.pm_stack} in @@ -704,7 +706,7 @@ let instr_suffices _then cut gls0 = let c_ctx,c_head = build_applist c_stat metas in let c_term = applist (mkVar c_id,List.map mkMeta metas) in let thus_tac gls= - thus_tac c_term c_head c_ctx gls in + thus_tac c_term (EConstr.of_constr c_head) c_ctx gls in tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id c_stat)) [tclTHENLIST [ assume_tac ctx; @@ -891,8 +893,9 @@ let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in - let is_dep = dependent (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl) in + let is_dep = dependent (project gls) (EConstr.of_constr casee) concl in let hd,args = decompose_app (special_whd gls ctyp) in + let ctyp = EConstr.Unsafe.to_constr ctyp in let (ind,u) = try destInd hd @@ -906,9 +909,10 @@ let build_per_info etype casee gls = let params,real_args = List.chop nparams args in let abstract_obj c body = let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in + let typ = EConstr.Unsafe.to_constr typ in lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in let pred= List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in + real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in is_dep, {per_casee=casee; per_ctype=ctyp; @@ -963,6 +967,7 @@ let register_nodep_subcase id= function let suppose_tac hyps gls0 = let info = get_its_info gls0 in let thesis = pf_concl gls0 in + let thesis = EConstr.Unsafe.to_constr thesis in let id = pf_get_new_id (Id.of_string "subcase_") gls0 in let clause = build_product (project gls0) hyps thesis in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in @@ -1132,7 +1137,7 @@ let rec build_product_dep pat_info per_info args body gls = with Not_found -> snd (st_assoc (Name id) pat_info.pat_aliases) in thesis_for obj typ per_info (pf_env gls) - | Plain -> pf_concl gls in + | Plain -> EConstr.Unsafe.to_constr (pf_concl gls) in mkProd (st.st_label,ptyp,lbody) | [] -> body @@ -1225,6 +1230,7 @@ let pop_stacks stacks = let hrec_for fix_id per_info gls obj_id = let obj=mkVar obj_id in let typ=pf_get_hyp_typ gls obj_id in + let typ = EConstr.Unsafe.to_constr typ in let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind); @@ -1269,14 +1275,16 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let env=pf_env gls in let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in let hd,all_args = decompose_app (special_whd gls ctyp) in + let ctyp = EConstr.Unsafe.to_constr ctyp in let ind', u = destInd hd in let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in + let typ = EConstr.Unsafe.to_constr typ in lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in let elim_pred = List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in + real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) concl)) in let case_info = Inductiveops.make_case_info env ind RegularStyle in let gen_arities = Inductive.arities_of_constructors (ind,u) spec in let f_ids typ = @@ -1341,13 +1349,13 @@ let understand_my_constr env sigma c concl = | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,Misctypes.IntroAnonymous,None) | rc -> map_glob_constr frob rc in - Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType (EConstr.of_constr concl)) (frob rawc) + Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) let my_refine c gls = let oc = { run = begin fun sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in - Sigma.Unsafe.of_pair (EConstr.of_constr c, sigma) + Sigma.Unsafe.of_pair (c, sigma) end } in Proofview.V82.of_tactic (Tactics.New.refine oc) gls diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index e39d17b52..f23f4ce7d 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -37,6 +37,7 @@ let start_deriving f suchthat lemma = let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in let evdref = ref sigma in let suchthat = Constrintern.interp_type_evars env' evdref suchthat in + let suchthat = EConstr.Unsafe.to_constr suchthat in TCons ( env' , !evdref , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 24d4346d9..2881b5333 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t= let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in + let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in match nam with Name id -> id | Anonymous -> dummy_bvid in diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index bed7a727f..38dae0b20 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -38,14 +38,14 @@ let wrap n b continue seq gls= []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> let id = NamedDecl.get_id nd in - if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) || + if occur_var env (project gls) id (pf_concl gls) || List.exists (occur_var_in_decl env (project gls) id) ctx then (aux (i-1) q (nd::ctx)) else add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then - add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in + add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in continue seq2 gls let basename_of_global=function diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 91cd102a2..fb0c22c2b 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -201,6 +201,7 @@ let extend_with_ref_list l seq gl = let f gr (seq,gl) = let gl, c = pf_eapply Evd.fresh_global gl gr in let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in + let typ = EConstr.Unsafe.to_constr typ in (add_formula Hyp gr typ seq gl,gl) in List.fold_right f l (seq,gl) @@ -216,6 +217,7 @@ let extend_with_auto_hints l seq gl= (try let (gr, _) = Termops.global_of_constr (project gl) c in let typ=(pf_unsafe_type_of gl c) in + let typ = EConstr.Unsafe.to_constr typ in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 656924e38..f4fa61a22 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -394,7 +394,7 @@ let rewrite_until_var arg_num eq_ids : tactic = *) let test_var g = let sigma = project g in - let _,args = destApp sigma (EConstr.of_constr (pf_concl g)) in + let _,args = destApp sigma (pf_concl g) in not ((isConstruct sigma args.(arg_num)) || isAppConstruct sigma args.(arg_num)) in let rec do_rewrite eq_ids g = @@ -551,7 +551,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (EConstr.of_constr (Typing.unsafe_type_of env sigma (mkVar hyp_id))), [hyp_id] + scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -602,7 +602,6 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in - let new_term_value_eq = EConstr.of_constr new_term_value_eq in (* compute the new value of the body *) let new_term_value = match EConstr.kind (project g') new_term_value_eq with @@ -615,7 +614,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = in let fun_body = mkLambda(Anonymous, - EConstr.of_constr (pf_unsafe_type_of g' term), + pf_unsafe_type_of g' term, Termops.replace_term (project g') term (mkRel 1) dyn_infos.info ) in @@ -708,9 +707,8 @@ let build_proof let t = dyn_info'.info in let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in - let g_nb_prod = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in + let g_nb_prod = nb_prod (project g) (pf_concl g) in let type_of_term = pf_unsafe_type_of g t in - let type_of_term = EConstr.of_constr type_of_term in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -722,7 +720,7 @@ let build_proof (fun g -> observe_tac "toto" ( tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t); (fun g' -> - let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in + let g'_nb_prod = nb_prod (project g') (pf_concl g') in let nb_instanciate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case @@ -742,7 +740,7 @@ let build_proof build_proof do_finalize_t {dyn_infos with info = t} g | Lambda(n,t,b) -> begin - match EConstr.kind sigma (EConstr.of_constr ( pf_concl g)) with + match EConstr.kind sigma (pf_concl g) with | Prod _ -> tclTHEN (Proofview.V82.of_tactic intro) @@ -914,7 +912,7 @@ let prove_rec_hyp_for_struct fix_info = (fun eq_hyps -> tclTHEN (rewrite_until_var (fix_info.idx) eq_hyps) (fun g -> - let _,pte_args = destApp (project g) (EConstr.of_constr (pf_concl g)) in + let _,pte_args = destApp (project g) (pf_concl g) in let rec_hyp_proof = mkApp(mkVar fix_info.name,array_get_start pte_args) in @@ -938,7 +936,7 @@ let generalize_non_dep hyp g = let hyp = get_id decl in if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep - || Termops.occur_var env (project g) hyp (EConstr.of_constr hyp_typ) + || Termops.occur_var env (project g) hyp hyp_typ || Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) @@ -1054,7 +1052,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in - let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in + let nb_intro_to_do = nb_prod (project g) (pf_concl g) in tclTHEN (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro)) ( @@ -1070,7 +1068,6 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic = fun g -> let princ_type = pf_concl g in - let princ_type = EConstr.of_constr princ_type in (* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *) (* Pp.msgnl (str "all_funs "); *) (* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *) @@ -1258,7 +1255,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let intros_after_fixes : tactic = fun gl -> - let ctxt,pte_app = (decompose_prod_assum (project gl) (EConstr.of_constr (pf_concl gl))) in + let ctxt,pte_app = (decompose_prod_assum (project gl) (pf_concl gl)) in let pte,pte_args = (decompose_app (project gl) pte_app) in try let pte = @@ -1431,12 +1428,12 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (project gls) (EConstr.of_constr (pf_unsafe_type_of gls (mkVar hrec))) in + let _,hrec_concl = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in let f = (fst (destApp (project gls) f_app)) in let rec backtrack : tactic = fun g -> - let f_app = Array.last (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))) in + let f_app = Array.last (snd (destApp (project g) (pf_concl g))) in match EConstr.kind (project g) f_app with | App(f',_) when eq_constr (project g) f' f -> tclIDTAC g | _ -> tclTHEN rewrite backtrack g @@ -1525,7 +1522,6 @@ let prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation gl = let princ_type = pf_concl gl in - let princ_type = EConstr.of_constr princ_type in let princ_info = compute_elim_sig (project gl) princ_type in let fresh_id = let avoid = ref (pf_ids_of_hyps gl) in @@ -1664,7 +1660,7 @@ let prove_principle_for_gen Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> let body = - let _,args = destApp (project gl') (EConstr.of_constr (pf_concl gl')) in + let _,args = destApp (project gl') (pf_concl gl') in Array.last args in let body_info rec_hyps = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d964002f9..ba01b3b04 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -493,7 +493,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con in let _ = evd := sigma in let l_schemes = - List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma) schemes + List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes in let i = ref (-1) in let sorts = @@ -671,7 +671,7 @@ let build_case_scheme fa = Indrec.build_case_analysis_scheme_default env sigma ind sf in let sigma = Sigma.to_evar_map sigma in - let scheme_type = (Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme) in + let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fc5a287ae..fd2f4bbd3 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -504,6 +504,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in + let rt_typ = EConstr.Unsafe.to_constr rt_typ in let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -612,6 +613,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in + let v_type = EConstr.Unsafe.to_constr v_type in let new_env = match n with Anonymous -> env @@ -629,7 +631,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in let (ind,_) = - try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ) + try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -661,7 +663,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in let (ind,_) = - try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ) + try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -706,7 +708,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in - Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr) + EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr)) ) el in (****** The next works only if the match is not dependent ****) @@ -755,6 +757,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let typ_of_id = Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in + let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in let raw_typ_of_id = Detyping.detype false [] env_with_pat_ids (Evd.from_env env) typ_of_id @@ -808,6 +811,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve if Id.Set.mem id this_pat_ids then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in + let typ_of_id = EConstr.Unsafe.to_constr typ_of_id in let raw_typ_of_id = Detyping.detype false [] new_env (Evd.from_env env) typ_of_id in @@ -1122,6 +1126,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in + let type_t' = EConstr.Unsafe.to_constr type_t' in let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e22fed391..1cde4420e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -78,11 +78,11 @@ let functional_induction with_clean c princl pat = ++Printer.pr_leconstr (mkConst c') ) in let princ = EConstr.of_constr princ in - (princ,NoBindings,EConstr.of_constr (Tacmach.pf_unsafe_type_of g' princ),g') + (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError(None,str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,EConstr.of_constr (Tacmach.pf_unsafe_type_of g princ),g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let sigma = Tacmach.project g' in let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index be82010d9..5cbec7743 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -263,7 +263,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let princ_type = nf_zeta princ_type in let princ_infos = Tactics.compute_elim_sig evd princ_type in (* The number of args of the function is then easily computable *) - let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in + let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* Since we cannot ensure that the functional principle is defined in the @@ -315,7 +315,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes List.fold_right (fun hid acc -> let type_of_hid = pf_unsafe_type_of g (mkVar hid) in - let type_of_hid = EConstr.of_constr type_of_hid in let sigma = project g in match EConstr.kind sigma type_of_hid with | Prod(_,_,t') -> @@ -503,7 +502,7 @@ and intros_with_rewrite_aux : tactic = fun g -> let eq_ind = make_eq () in let sigma = project g in - match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with + match EConstr.kind sigma (pf_concl g) with | Prod(_,t,t') -> begin match EConstr.kind sigma t with @@ -591,7 +590,7 @@ and intros_with_rewrite_aux : tactic = let rec reflexivity_with_destruct_cases g = let destruct_case () = try - match EConstr.kind (project g) (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))).(2) with + match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with | Case(_,_,v,_) -> tclTHENSEQ[ Proofview.V82.of_tactic (simplest_case v); @@ -608,7 +607,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match EConstr.kind (project g) (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with + match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g @@ -674,12 +673,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let f = funcs.(i) in let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in let princ_type = pf_unsafe_type_of g graph_principle in - let princ_type = EConstr.of_constr princ_type in let princ_infos = Tactics.compute_elim_sig (project g) princ_type in (* Then we get the number of argument of the function and compute a fresh name for each of them *) - let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in + let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* and fresh names for res H and the principle (cf bug bug #1174) *) @@ -937,7 +935,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let revert_graph kn post_tac hid g = let sigma = project g in let typ = pf_unsafe_type_of g (mkVar hid) in - let typ = EConstr.of_constr typ in match EConstr.kind sigma typ with | App(i,args) when isInd sigma i -> let ((kn',num) as ind'),u = destInd sigma i in @@ -990,7 +987,6 @@ let functional_inversion kn hid fconst f_correct : tactic = let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let sigma = project g in let type_of_h = pf_unsafe_type_of g (mkVar hid) in - let type_of_h = EConstr.of_constr type_of_h in match EConstr.kind sigma type_of_h with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> let pre_tac,f_args,res = @@ -1044,7 +1040,6 @@ let invfun qhyp f g = (fun hid -> Proofview.V82.tactic begin fun g -> let sigma = project g in let hyp_typ = pf_unsafe_type_of g (mkVar hid) in - let hyp_typ = EConstr.of_constr hyp_typ in match EConstr.kind sigma hyp_typ with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> begin diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a80a7b5e7..adbdb1eb7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -123,7 +123,7 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = EConstr.of_constr (rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] - (pf_unsafe_type_of gls c)) + (EConstr.Unsafe.to_constr (pf_unsafe_type_of gls c))) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -412,7 +412,6 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = h_intros to_intros; (fun g' -> let ty_teq = pf_unsafe_type_of g' (mkVar heq) in - let ty_teq = EConstr.of_constr ty_teq in let teq_lhs,teq_rhs = let _,args = try destApp (project g') ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -522,19 +521,19 @@ let rec prove_lt hyple g = let sigma = project g in begin try - let (varx,varz) = match decompose_app sigma (EConstr.of_constr (pf_concl g)) with + let (varx,varz) = match decompose_app sigma (pf_concl g) with | _, x::z::_ when isVar sigma x && isVar sigma z -> x, z | _ -> assert false in let h = List.find (fun id -> - match decompose_app sigma (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with + match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with | _, t::_ -> EConstr.eq_constr sigma t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app sigma (EConstr.of_constr (pf_unsafe_type_of g (mkVar h)))))) in + List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) @@ -698,7 +697,6 @@ let mkDestructEq : then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_unsafe_type_of g expr in - let type_of_expr = EConstr.of_constr type_of_expr in let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> @@ -707,7 +705,7 @@ let mkDestructEq : (fun g2 -> let changefun patvars = { run = fun sigma -> let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in - let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in + let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) in Sigma (c, sigma, p) } in Proofview.V82.of_tactic (change_in_concl None changefun) g2); @@ -846,7 +844,7 @@ let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = let rec prove_le g = let sigma = project g in let x,z = - let _,args = decompose_app sigma (EConstr.of_constr (pf_concl g)) in + let _,args = decompose_app sigma (pf_concl g) in (List.hd args,List.hd (List.tl args)) in tclFIRST[ @@ -857,9 +855,8 @@ let rec prove_le g = let matching_fun = pf_is_matching g (Pattern.PApp(Pattern.PRef (reference_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in - let (h,t) = List.find (fun (_,t) -> matching_fun (EConstr.of_constr t)) (pf_hyps_types g) + let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in - let t = EConstr.of_constr t in let y = let _,args = decompose_app sigma t in List.hd (List.tl args) @@ -1350,7 +1347,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ] gls) (fun g -> let sigma = project g in - match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with + match EConstr.kind sigma (pf_concl g) with | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) -> Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g | _ -> @@ -1523,9 +1520,11 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = ref (Evd.from_env env) in let function_type = interp_type_evars env evd type_of_f in + let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let ty = interp_type_evars env evd ~impls:rec_impls eq in + let ty = EConstr.Unsafe.to_constr ty in let evm, nf = Evarutil.nf_evars_and_universes !evd in let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ced572466..a2346cc90 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1606,6 +1606,7 @@ let rec parse_hyps gl parse_arith env tg hyps = match hyps with | [] -> ([],env,tg) | (i,t)::l -> + let t = EConstr.Unsafe.to_constr t in let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in try let (c,env,tg) = parse_formula gl parse_arith env tg t in @@ -1713,7 +1714,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ("__varmap", vm, Term.mkApp( coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl)) + (EConstr.Unsafe.to_constr (Tacmach.pf_concl gl))) ] end } @@ -1964,6 +1965,7 @@ let micromega_gen Proofview.Goal.nf_enter { enter = begin fun gl -> let gl = Tacmach.New.of_old (fun x -> x) gl in let concl = Tacmach.pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let hyps = Tacmach.pf_hyps_types gl in try let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in @@ -2051,7 +2053,7 @@ let micromega_order_changer cert env ff = [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.pf_concl gl))); + (EConstr.Unsafe.to_constr (Tacmach.pf_concl gl)))); (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) ] end } @@ -2072,6 +2074,7 @@ let micromega_genr prover tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let gl = Tacmach.New.of_old (fun x -> x) gl in let concl = Tacmach.pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let hyps = Tacmach.pf_hyps_types gl in try diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 51790f4c9..665486272 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -38,9 +38,9 @@ open OmegaSolver let elim_id id = Proofview.Goal.nf_enter { enter = begin fun gl -> - simplest_elim (EConstr.of_constr (Tacmach.New.pf_global id gl)) + simplest_elim (Tacmach.New.pf_global id gl) end } -let resolve_id id gl = Proofview.V82.of_tactic (apply (EConstr.of_constr (pf_global gl id))) gl +let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl let timing timer_name f arg = f arg @@ -568,7 +568,7 @@ let abstract_path typ path t = mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur let focused_simpl path gl = - let newc = context (fun i t -> EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr t))) (List.rev path) (pf_concl gl) in + let newc = context (fun i t -> EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr t))) (List.rev path) (EConstr.Unsafe.to_constr (pf_concl gl)) in let newc = EConstr.of_constr newc in Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl @@ -632,6 +632,7 @@ let mkNewMeta () = mkMeta (Evarutil.new_meta()) let clever_rewrite_base_poly typ p result theorem gl = let full = pf_concl gl in + let full = EConstr.Unsafe.to_constr full in let (abstracted,occ) = abstract_path typ (List.rev p) full in let t = applist @@ -663,6 +664,7 @@ let clever_rewrite_gen_nat p result (t,args) = let clever_rewrite p vpath t gl = let full = pf_concl gl in + let full = EConstr.Unsafe.to_constr full in let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in let vargs = List.map (fun p -> occurrence p occ) vpath in let t' = applist(t, (vargs @ [abstracted])) in @@ -1424,6 +1426,7 @@ let coq_omega = Proofview.Goal.nf_enter { enter = begin fun gl -> clear_constr_tables (); let hyps_types = Tacmach.New.pf_hyps_types gl in + let hyps_types = List.map (on_snd EConstr.Unsafe.to_constr) hyps_types in let destructure_omega = Tacmach.New.of_old destructure_omega gl in let tactic_normalisation, system = List.fold_left destructure_omega ([],[]) hyps_types in @@ -1607,6 +1610,7 @@ let nat_inject = with e when catchable_exception e -> loop lit end in let hyps_types = Tacmach.New.pf_hyps_types gl in + let hyps_types = List.map (on_snd EConstr.Unsafe.to_constr) hyps_types in loop (List.rev hyps_types) end } @@ -1722,7 +1726,7 @@ let destructure_hyps = | Kimp(t1,t2) -> (* t1 and t2 might be in Type rather than Prop. For t1, the decidability check will ensure being Prop. *) - if is_Prop (type_of (EConstr.of_constr t2)) + if is_Prop (EConstr.Unsafe.to_constr (type_of (EConstr.of_constr t2))) then let d1 = decidability t1 in Tacticals.New.tclTHENLIST [ diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 87276f5df..edf34607b 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -459,8 +459,7 @@ let quote f lid = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let f = Tacmach.New.pf_global f gl in - let f = EConstr.of_constr f in - let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in let ivs = compute_ivs f cl gl in let concl = Proofview.Goal.concl gl in let quoted_terms = quote_terms env sigma ivs [concl] in @@ -478,8 +477,7 @@ let gen_quote cont c f lid = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let f = Tacmach.New.pf_global f gl in - let f = EConstr.of_constr f in - let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in + let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in let ivs = compute_ivs f cl gl in let quoted_terms = quote_terms env sigma ivs [c] in let (p, vm) = match quoted_terms with diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index ab5033601..cfe14b230 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -740,6 +740,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = let reify_gl env gl = let concl = Tacmach.pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let t_concl = Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in if !debug then begin @@ -748,6 +749,7 @@ let reify_gl env gl = end; let rec loop = function (i,t) :: lhyps -> + let t = EConstr.Unsafe.to_constr t in let t' = oproposition_of_constr env (false,[],i,[]) gl t in if !debug then begin Printf.printf " %s: " (Names.Id.to_string i); diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 981ce2a61..475380512 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -262,8 +262,9 @@ let rtauto_tac gls= let gl=pf_concl gls in let _= if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) (EConstr.of_constr gl) != InProp + (pf_env gls) (Tacmach.project gls) gl != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in + let gl = EConstr.Unsafe.to_constr gl in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in let formula= diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 358ea5685..f52557095 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -142,7 +142,7 @@ let ic c = let env = Global.env() in let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_open_constr env sigma c in - (sigma, EConstr.of_constr c) + (sigma, c) let ic_unsafe c = (*FIXME remove *) let env = Global.env() in @@ -505,8 +505,6 @@ let ring_equality env evd (r,add,mul,opp,req) = | None -> plapp evd coq_eq_smorph [|r;add;mul|] in let setoid = Typing.e_solve_evars env evd setoid in let op_morph = Typing.e_solve_evars env evd op_morph in - let setoid = EConstr.of_constr setoid in - let op_morph = EConstr.of_constr op_morph in (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in @@ -594,6 +592,7 @@ let make_hyp_list env evd lH = (plapp evd coq_nil [|carrier|]) in let l' = Typing.e_solve_evars env evd l in + let l' = EConstr.Unsafe.to_constr l' in Evarutil.nf_evars_universes !evd l' let interp_power env evd pow = @@ -756,7 +755,7 @@ let ring_lookup (f : Value.t) lH rl t = let rl = make_args_list sigma rl t in let evdref = ref sigma in let e = find_ring_structure env sigma rl in - let rl = carg (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in let lH = carg (make_hyp_list env evdref lH) in let ring = ltac_ring_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl])) @@ -1039,7 +1038,7 @@ let field_lookup (f : Value.t) lH rl t = let rl = make_args_list sigma rl t in let evdref = ref sigma in let e = find_field_structure env sigma rl in - let rl = carg (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in + let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in let lH = carg (make_hyp_list env evdref lH) in let field = ltac_field_structure e in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl])) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 9dcc6c4cc..eb5f401e3 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1353,6 +1353,7 @@ let fill_occ_term env cl occ sigma0 (sigma, t) = let pf_fill_occ_term gl occ t = let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t @@ -1388,6 +1389,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl = let pat = interp_rpattern arg_ist gl arg in let sigma0 = project gl in let concl0 = pf_concl gl in + let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in @@ -1416,6 +1418,7 @@ let ssrinstancesof ist arg gl = let ok rhs lhs ise = true in (* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) let env, sigma, concl = pf_env gl, project gl, pf_concl gl in + let concl = EConstr.Unsafe.to_constr concl in let sigma0, cpat = interp_cpattern ist gl arg None in let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 565a9725c..eea94f021 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2076,7 +2076,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env !evdref - {uj_val = ty; uj_type = EConstr.of_constr (Typing.unsafe_type_of env !evdref ty)} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index a42061f28..e18625c42 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -377,7 +377,7 @@ and cbv_norm_value info = function (* reduction under binders *) (* with profiling *) let cbv_norm infos constr = let constr = EConstr.Unsafe.to_constr constr in - with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)) + EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))) type cbv_infos = cbv_value infos diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 3d1745767..b014af2c7 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -8,6 +8,7 @@ open Names open Term +open EConstr open Environ open CClosure open Esubst @@ -19,10 +20,13 @@ open Esubst type cbv_infos val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos -val cbv_norm : cbv_infos -> EConstr.constr -> constr +val cbv_norm : cbv_infos -> constr -> constr (*********************************************************************** i This is for cbv debug *) + +open Term + type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f569d9fc4..ead44cee2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -194,7 +194,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> let term = co x in - EConstr.of_constr (Typing.e_solve_evars env evdref term)) + Typing.e_solve_evars env evdref term) in if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then (* Second-order unification needed. *) @@ -302,7 +302,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) with NoSubtacCoercion -> let typ = Typing.unsafe_type_of env evm c in let typ' = Typing.unsafe_type_of env evm c' in - coerce_application (EConstr.of_constr typ) (EConstr.of_constr typ') c c' l l') + coerce_application typ typ' c c' l l') else subco () | x, y when EConstr.eq_constr !evdref c c' -> @@ -310,7 +310,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) let evm = !evdref in let lam_type = Typing.unsafe_type_of env evm c in let lam_type' = Typing.unsafe_type_of env evm c' in - coerce_application (EConstr.of_constr lam_type) (EConstr.of_constr lam_type') c c' l l' + coerce_application lam_type lam_type' c c' l l' else subco () | _ -> subco ()) | _, _ -> subco () @@ -341,7 +341,7 @@ let app_coercion env evdref coercion v = | None -> v | Some f -> let v' = Typing.e_solve_evars env evdref (f v) in - whd_betaiota !evdref (EConstr.of_constr v') + whd_betaiota !evdref v' let coerce_itf loc env evd v t c1 = let evdref = ref evd in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 09b99983c..f76f608d0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -524,7 +524,6 @@ let pretype_ref loc evdref env ref us = let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in let ty = unsafe_type_of env.ExtraEnv.env evd c in - let ty = EConstr.of_constr ty in make_judge c ty let judge_of_Type loc evd s = @@ -1194,16 +1193,16 @@ let understand let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in - (sigma, EConstr.Unsafe.to_constr c) + (sigma, c) let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in evdref := sigma; - EConstr.Unsafe.to_constr c + c let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in - (sigma, EConstr.Unsafe.to_constr c) + (sigma, c) let constr_flags = { use_typeclasses = true; @@ -1225,7 +1224,6 @@ let type_uconstr ?(flags = constr_flags) } in let sigma = Sigma.to_evar_map sigma in let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) end } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index a1602088a..825d73f1f 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -76,10 +76,10 @@ val allow_anonymous_refs : bool ref evar_map is modified explicitly or by side-effect. *) val understand_tcc : ?flags:inference_flags -> env -> evar_map -> - ?expected_type:typing_constraint -> glob_constr -> open_constr + ?expected_type:typing_constraint -> glob_constr -> evar_map * EConstr.constr val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> - ?expected_type:typing_constraint -> glob_constr -> constr + ?expected_type:typing_constraint -> glob_constr -> EConstr.constr (** More general entry point with evars from ltac *) @@ -95,7 +95,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr + typing_constraint -> glob_constr -> evar_map * EConstr.constr (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3fc01c86c..2b496f926 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1133,7 +1133,7 @@ let fold_commands cl env sigma c = (* call by value reduction functions *) let cbv_norm_flags flags env sigma t = - EConstr.of_constr (cbv_norm (create_cbv_infos flags env sigma) t) + cbv_norm (create_cbv_infos flags env sigma) t let cbv_beta = cbv_norm_flags beta empty_env let cbv_betaiota = cbv_norm_flags betaiota empty_env diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d24160ea5..7baff421f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -376,7 +376,7 @@ let unsafe_type_of env evd c = let evdref = ref evd in let env = enrich_env env evdref in let j = execute env evdref c in - EConstr.Unsafe.to_constr j.uj_type + j.uj_type (* Sort of a type *) @@ -411,6 +411,6 @@ let e_solve_evars env evdref c = let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) - nf_evar !evdref (EConstr.Unsafe.to_constr c) + EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr c)) -let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c)) +let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index bf26358a2..91134b499 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -9,46 +9,47 @@ open Names open Term open Environ +open EConstr open Evd (** This module provides the typing machine with existential variables and universes. *) (** Typecheck a term and return its type. May trigger an evarmap leak. *) -val unsafe_type_of : env -> evar_map -> EConstr.constr -> types +val unsafe_type_of : env -> evar_map -> constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * EConstr.types +val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Variant of [type_of] using references instead of state-passing. *) -val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> EConstr.types +val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) -val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts +val e_sort_of : env -> evar_map ref -> types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit +val e_check : env -> evar_map ref -> constr -> types -> unit (** Returns the instantiated type of a metavariable *) -val meta_type : evar_map -> metavariable -> EConstr.types +val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) -val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr +val e_solve_evars : env -> evar_map ref -> constr -> constr (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) -val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr -> +val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit (** Raise an error message if bodies have types not unifiable with the expected ones *) val check_type_fixpoint : Loc.t -> env -> evar_map ref -> - Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> unit + Names.Name.t array -> types array -> unsafe_judgment array -> unit -val judge_of_prop : EConstr.unsafe_judgment -val judge_of_set : EConstr.unsafe_judgment +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment val judge_of_abstraction : Environ.env -> Name.t -> - EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment + unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> - EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment + unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c6fad1a34..5bb865310 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1228,7 +1228,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in - apprec n c (EConstr.of_constr (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c)) Sigma.refl evd + apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd let is_mimick_head sigma ts f = match EConstr.kind sigma f with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 7269c61e3..e580bccc3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -133,7 +133,7 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t)) +let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) (******************************************************************) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0d65faf12..1ddb67edd 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -27,9 +27,9 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c env evd = - if Termops.occur_evar evd evk (EConstr.of_constr c) then - Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c); - let evd = define evk c evd in + if Termops.occur_evar evd evk c then + Pretype_errors.error_occur_check env evd evk c; + let evd = define evk (EConstr.Unsafe.to_constr c) evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in match List.fold_left diff --git a/proofs/logic.ml b/proofs/logic.ml index 8b890f6f8..59ce8ffa6 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -330,7 +330,7 @@ let meta_free_prefix sigma a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then unsafe_type_of env sigma (EConstr.of_constr c) + if !check then EConstr.Unsafe.to_constr (unsafe_type_of env sigma (EConstr.of_constr c)) else EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 3641ad74d..2fab026ea 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -46,11 +46,11 @@ let test_conversion cb env sigma c1 c2 = let c2 = EConstr.Unsafe.to_constr c2 in test_conversion cb env sigma c1 c2 -let pf_concl gls = EConstr.Unsafe.to_constr (Goal.V82.concl (project gls) (sig_it gls)) +let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) let pf_hyps_types gls = let sign = Environ.named_context (pf_env gls) in List.map (function LocalAssum (id,x) - | LocalDef (id,_,x) -> id, x) + | LocalDef (id,_,x) -> id, EConstr.of_constr x) sign let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id @@ -64,7 +64,7 @@ let pf_get_hyp gls id = raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - id |> pf_get_hyp gls |> NamedDecl.get_type + id |> pf_get_hyp gls |> NamedDecl.get_type |> EConstr.of_constr let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -77,7 +77,7 @@ let pf_get_new_ids ids gls = (fun id acc -> (next_ident_away id (acc@avoid))::acc) ids [] -let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id +let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -103,7 +103,7 @@ let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL -let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) +let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind @@ -173,7 +173,7 @@ module New = struct (** We only check for the existence of an [id] in [hyps] *) let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in - Constrintern.construct_reference hyps id + EConstr.of_constr (Constrintern.construct_reference hyps id) let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl @@ -205,13 +205,13 @@ module New = struct sign let pf_get_hyp_typ id gl = - pf_get_hyp id gl |> NamedDecl.get_type + pf_get_hyp id gl |> NamedDecl.get_type |> EConstr.of_constr let pf_hyps_types gl = let env = Proofview.Goal.env gl in let sign = Environ.named_context env in List.map (function LocalAssum (id,x) - | LocalDef (id,_,x) -> id, x) + | LocalDef (id,_,x) -> id, EConstr.of_constr x) sign let pf_last_hyp gl = @@ -241,6 +241,6 @@ module New = struct let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = nf_evar (project gl) t + let pf_nf_evar gl t = EConstr.of_constr (nf_evar (project gl) (EConstr.Unsafe.to_constr t)) end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f0471bf66..efc3dbf55 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -9,6 +9,7 @@ open Names open Term open Environ +open EConstr open Evd open Proof_type open Redexpr @@ -40,9 +41,9 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_unsafe_type_of : goal sigma -> EConstr.constr -> types -val pf_type_of : goal sigma -> EConstr.constr -> evar_map * EConstr.types -val pf_hnf_type_of : goal sigma -> EConstr.constr -> EConstr.types +val pf_unsafe_type_of : goal sigma -> constr -> types +val pf_type_of : goal sigma -> constr -> evar_map * types +val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types @@ -50,7 +51,7 @@ val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list -val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * EConstr.constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a @@ -63,35 +64,35 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_all : goal sigma -> EConstr.constr -> EConstr.constr -val pf_hnf_constr : goal sigma -> EConstr.constr -> EConstr.constr -val pf_nf : goal sigma -> EConstr.constr -> EConstr.constr -val pf_nf_betaiota : goal sigma -> EConstr.constr -> EConstr.constr -val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types -val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * EConstr.types -val pf_compute : goal sigma -> EConstr.constr -> EConstr.constr +val pf_whd_all : goal sigma -> constr -> constr +val pf_hnf_constr : goal sigma -> constr -> constr +val pf_nf : goal sigma -> constr -> constr +val pf_nf_betaiota : goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types +val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types +val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> EConstr.constr -> EConstr.constr + -> goal sigma -> constr -> constr val pf_const_value : goal sigma -> pconstant -> constr -val pf_conv_x : goal sigma -> EConstr.constr -> EConstr.constr -> bool -val pf_conv_x_leq : goal sigma -> EConstr.constr -> EConstr.constr -> bool +val pf_conv_x : goal sigma -> constr -> constr -> bool +val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool +val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map +val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> EConstr.types -> tactic -val refine_no_check : EConstr.constr -> tactic +val internal_cut_no_check : bool -> Id.t -> types -> tactic +val refine_no_check : constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> EConstr.types -> tactic -val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic -val refine : EConstr.constr -> tactic +val internal_cut : bool -> Id.t -> types -> tactic +val internal_cut_rev : bool -> Id.t -> types -> tactic +val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds @@ -106,11 +107,11 @@ module New : sig val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env - val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types - val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * EConstr.types - val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list @@ -120,16 +121,16 @@ module New : sig val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> EConstr.types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * EConstr.types + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types - val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types - val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> EConstr.types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr - val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr - val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 9942e911a..e3f1c1ac2 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -461,6 +461,7 @@ let start_proof_com ?inference_hook kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in + let t' = EConstr.Unsafe.to_constr t' in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f2e98ee01..f43f4b250 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -257,7 +257,7 @@ type hypinfo = { let decompose_applied_relation metas env sigma c ctype left2right = let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr ty) in + let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in let eqclause = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) @@ -274,6 +274,8 @@ let decompose_applied_relation metas env sigma c ctype left2right = let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) in + let ty = EConstr.Unsafe.to_constr ty in + let ty1 = EConstr.Unsafe.to_constr ty1 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; @@ -284,9 +286,8 @@ let decompose_applied_relation metas env sigma c ctype left2right = match find_rel ctype with | Some c -> Some c | None -> - let ctx,t' = Reductionops.splay_prod_assum env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) - let t' = EConstr.Unsafe.to_constr t' in - match find_rel (Term.it_mkProd_or_LetIn t' ctx) with + let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) + match find_rel (it_mkProd_or_LetIn t' ctx) with | Some c -> Some c | None -> None @@ -296,7 +297,7 @@ let find_applied_relation metas loc env sigma c left2right = | Some c -> c | None -> user_err ~loc ~hdr:"decompose_applied_relation" - (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ + (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 84ca0aa8f..fa2c21ac3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -227,7 +227,6 @@ let e_give_exact flags poly (c,clenv) gl = else c, gl in let t1 = pf_unsafe_type_of gl c in - let t1 = EConstr.of_constr t1 in Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> @@ -1515,7 +1514,6 @@ let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in let cty = pf_unsafe_type_of gl c in - let cty = EConstr.of_constr cty in let ce = mk_clenv_from gl (c,cty) in let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),0,ce) } in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index afc7e1547..a3a448aad 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -116,7 +116,6 @@ let contradiction_term (c,lbind as cl) = let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in - let typ = EConstr.of_constr typ in let _, ccl = splay_prod env sigma typ in if is_empty_type sigma ccl then Tacticals.New.tclTHEN diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 92e59c5ce..01f21910c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -32,7 +32,6 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter { enter = begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in - let t1 = EConstr.of_constr t1 in let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then @@ -290,7 +289,7 @@ module SearchProblem = struct in let rec_tacs = let l = - let concl = Reductionops.nf_evar (project g)(pf_concl g) in + let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in let concl = EConstr.of_constr concl in filter_tactics s.tacres (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) @@ -516,7 +515,7 @@ let autounfold_one db cl = (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db in let did, c' = unfold_head env sigma st - (match cl with Some (id, _) -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl) | None -> concl) + (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) in if did then match cl with diff --git a/tactics/elim.ml b/tactics/elim.ml index ef848c2e1..a4158f821 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -82,7 +82,6 @@ let general_decompose recognizer c = let type_of = pf_unsafe_type_of gl in let sigma = project gl in let typc = type_of c in - let typc = EConstr.of_constr typc in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId @@ -136,7 +135,6 @@ let induction_trailer abs_i abs_j bargs = (fun id -> Proofview.Goal.nf_enter { enter = begin fun gl -> let idty = pf_unsafe_type_of gl (mkVar id) in - let idty = EConstr.of_constr idty in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 16e0d9684..df60f2c66 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -163,7 +163,6 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with | a1 :: largs, a2 :: rargs -> Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl a1 in - let rectype = EConstr.of_constr rectype in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in let subtacs = @@ -236,7 +235,6 @@ let decideEquality rectype = let compare c1 c2 = Proofview.Goal.enter { enter = begin fun gl -> let rectype = pf_unsafe_type_of gl c1 in - let rectype = EConstr.of_constr rectype in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro diff --git a/tactics/equality.ml b/tactics/equality.ml index e1c39bb34..7dcfd419e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -311,7 +311,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = in let typ = match cls with | None -> pf_nf_concl gl - | Some id -> EConstr.of_constr (pf_get_hyp_typ id (Proofview.Goal.assume gl)) + | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl) in let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) @@ -407,7 +407,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = let type_of_clause cls gl = match cls with | None -> Proofview.Goal.concl gl - | Some id -> EConstr.of_constr (pf_get_hyp_typ id gl) + | Some id -> pf_get_hyp_typ id gl let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> @@ -950,7 +950,6 @@ let gen_absurdity id = Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in - let hyp_typ = EConstr.of_constr hyp_typ in if is_empty_type sigma hyp_typ then simplest_elim (mkVar id) @@ -1027,7 +1026,6 @@ let onEquality with_evars tac (c,lbindc) = let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in - let t = EConstr.of_constr t in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in @@ -1136,7 +1134,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, EConstr.of_constr (unsafe_type_of env sigma (mkRel i)))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1184,7 +1182,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) p_i !evdref in + let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in dflt with Evarconv.UnableToUnify _ -> @@ -1200,7 +1198,6 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = match evopt with | Some w -> let w_type = unsafe_type_of env !evdref w in - let w_type = EConstr.of_constr w_type in if Evarconv.e_cumul env evdref w_type a then let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in let exist_term = EConstr.of_constr exist_term in @@ -1290,7 +1287,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,EConstr.of_constr (unsafe_type_of env sigma c)) + | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1345,7 +1342,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|EConstr.of_constr (pf_unsafe_type_of gl ar1.(3));ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let inj2 = EConstr.of_constr inj2 in @@ -1613,7 +1610,6 @@ let cutSubstInHyp l2r eqn id = let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in - let typ = EConstr.of_constr typ in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in let tac = @@ -1702,8 +1698,7 @@ let is_eq_x gl x d = | Var id' -> Id.equal id id' | _ -> false in - let c = pf_nf_evar gl (NamedDecl.get_type d) in - let c = EConstr.of_constr c in + let c = pf_nf_evar gl (EConstr.of_constr (NamedDecl.get_type d)) in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false)) @@ -1852,7 +1847,6 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let find_eq_data_decompose = find_eq_data_decompose gl in let test (_,c) = try - let c = EConstr.of_constr c in let lbeq,u,(_,x,y) = find_eq_data_decompose c in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; diff --git a/tactics/hints.ml b/tactics/hints.ml index 2446b6996..851e9f01f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -919,7 +919,7 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in + let t = hnf_constr env sigma (unsafe_type_of env sigma c) in let hd = head_constr sigma t in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; @@ -1239,7 +1239,6 @@ let interp_hints poly = let sigma = Evd.from_env env in let f poly c = let evd,c = Constrintern.interp_open_constr env sigma c in - let c = EConstr.of_constr c in prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index fa114a3d3..607d6d2a9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -442,7 +442,7 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl e1 in (EConstr.of_constr t,e1,e2) + let t = pf_unsafe_type_of gl e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if pf_conv_x gl t1 t2 then (t1,e1,e2) diff --git a/tactics/inv.ml b/tactics/inv.ml index a398e04dd..426749a75 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -346,7 +346,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = let sigma = project gl in (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl (EConstr.of_constr hyp) in + let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 @@ -443,7 +443,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c)) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in CErrors.user_err msg diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 2d59285e6..3199623e7 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -258,7 +258,6 @@ let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () in let evd = ref (Evd.from_env env) in let c = Constrintern.interp_type_evars env evd com in - let c = EConstr.of_constr c in let sigma, sort = Pretyping.interp_sort !evd comsort in try add_inversion_lemma na env sigma c sort bool tac diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index d79a74b36..89acc149c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -128,7 +128,7 @@ let onClauseLR tac cl gls = tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls let ifOnHyp pred tac1 tac2 id gl = - if pred (id,EConstr.of_constr (pf_get_hyp_typ gl id)) then + if pred (id,pf_get_hyp_typ gl id) then tac1 id gl else tac2 id gl @@ -248,10 +248,10 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = Array.map2 analrec lc lrecargs let elimination_sort_of_goal gl = - pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_concl gl)) + pf_apply Retyping.get_sort_family_of gl (pf_concl gl) let elimination_sort_of_hyp id gl = - pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_get_hyp_typ gl id)) + pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id) let elimination_sort_of_clause = function | None -> elimination_sort_of_goal @@ -269,21 +269,22 @@ let pf_constr_of_global gr k = let gl_make_elim ind gl = let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in - pf_apply Evd.fresh_global gl gr + let (sigma, c) = pf_apply Evd.fresh_global gl gr in + (sigma, EConstr.of_constr c) let gl_make_case_dep ind gl = let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true (elimination_sort_of_goal gl) in - (Sigma.to_evar_map sigma, r) + (Sigma.to_evar_map sigma, EConstr.of_constr r) let gl_make_case_nodep ind gl = let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false (elimination_sort_of_goal gl) in - (Sigma.to_evar_map sigma, r) + (Sigma.to_evar_map sigma, EConstr.of_constr r) let make_elim_branch_assumptions ba gl = let assums = @@ -583,7 +584,6 @@ module New = struct let ifOnHyp pred tac1 tac2 id = Proofview.Goal.nf_enter { enter = begin fun gl -> let typ = Tacmach.New.pf_get_hyp_typ id gl in - let typ = EConstr.of_constr typ in if pred (id,typ) then tac1 id else @@ -630,7 +630,7 @@ module New = struct (Proofview.Goal.nf_enter { enter = begin fun gl -> let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (EConstr.of_constr elim,EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim)))) gl in + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -642,7 +642,7 @@ module New = struct | Meta p -> p | _ -> let name_elim = - match kind_of_term elim with + match EConstr.kind sigma elim with | Const (kn, _) -> string_of_con kn | Var id -> string_of_id id | _ -> "\b" @@ -680,7 +680,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter { enter = begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c)) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim @@ -715,7 +715,7 @@ module New = struct let elimination_sort_of_hyp id gl = (** Retyping will expand evars anyway. *) let c = pf_get_hyp_typ id (Goal.assume gl) in - pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr c) + pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_clause id gl = match id with | None -> elimination_sort_of_goal gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dcaa15fd8..f79f7f1a8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1260,7 +1260,6 @@ let cut c = try (** Backward compat: ensure that [c] is well-typed. *) let typ = Typing.unsafe_type_of env sigma c in - let typ = EConstr.of_constr typ in let typ = whd_all env sigma typ in match EConstr.kind sigma typ with | Sort _ -> true @@ -1515,7 +1514,7 @@ let find_ind_eliminator ind s gl = evd, c let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c)) in + let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); @@ -1891,7 +1890,6 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in - let t' = EConstr.of_constr t' in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (local_assum (Anonymous,t')) naming gl in let rec aux idstoclear with_destruct c = @@ -1949,7 +1947,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in - match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c))) with + match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in @@ -2004,7 +2002,7 @@ let exact_proof c = Proofview.Goal.nf_enter { enter = begin fun gl -> Refine.refine { run = begin fun sigma -> let sigma = Sigma.to_evar_map sigma in - let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (EConstr.Unsafe.to_constr (pf_concl gl)) in + let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in let c = EConstr.of_constr c in let sigma = Evd.merge_universe_context sigma ctx in Sigma.Unsafe.of_pair (c, sigma) @@ -2326,7 +2324,6 @@ let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in - let t = EConstr.of_constr t in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> @@ -2341,7 +2338,6 @@ let intro_or_and_pattern loc with_evars bracketed ll thin tac id = Proofview.Goal.enter { enter = begin fun gl -> let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in - let t = EConstr.of_constr t in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let branchsigns = compute_constructor_signatures false ind in let nv_with_let = Array.map List.length branchsigns in @@ -2366,7 +2362,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let sigma = Tacmach.New.project gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in - let t = whd_all (EConstr.of_constr (type_of (mkVar id))) in + let t = whd_all (type_of (mkVar id)) in let eqtac, thin = match match_with_equality_type sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then @@ -2774,7 +2770,6 @@ let forward b usetac ipat c = | None -> Proofview.Goal.enter { enter = begin fun gl -> let t = Tacmach.New.pf_unsafe_type_of gl c in - let t = EConstr.of_constr t in let sigma = Tacmach.New.project gl in let hd = head_ident sigma c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c) @@ -2861,7 +2856,7 @@ let old_generalize_dep ?(with_let=false) c gl = -> id::tothin | _ -> tothin in - let cl' = it_mkNamedProd_or_LetIn (EConstr.of_constr (Tacmach.pf_concl gl)) to_quantify in + let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in let body = if with_let then match EConstr.kind sigma c with @@ -3222,7 +3217,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in - let tmptyp0 = EConstr.of_constr tmptyp0 in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in let typ0 = reduce_to_quantified_ref indref tmptyp0 in let prods, indtyp = decompose_prod_assum sigma typ0 in @@ -3266,7 +3260,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -3660,7 +3654,6 @@ let abstract_args gl generalize_vars dep id defined f args = let sigma = ref (Tacmach.project gl) in let env = Tacmach.pf_env gl in let concl = Tacmach.pf_concl gl in - let concl = EConstr.of_constr concl in let dep = dep || local_occur_var !sigma id concl in let avoid = ref [] in let get_id name = @@ -3681,7 +3674,6 @@ let abstract_args gl generalize_vars dep id defined f args = in let ty = EConstr.of_constr ty in let argty = Tacmach.pf_unsafe_type_of gl arg in - let argty = EConstr.of_constr argty in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in let () = sigma := sigma' in let lenctx = List.length ctx in @@ -3723,7 +3715,6 @@ let abstract_args gl generalize_vars dep id defined f args = in if dogen then let tyf' = Tacmach.pf_unsafe_type_of gl f' in - let tyf' = EConstr.of_constr tyf' in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in @@ -3739,7 +3730,6 @@ let abstract_args gl generalize_vars dep id defined f args = else None, c' in let typ = Tacmach.pf_get_hyp_typ gl id in - let typ = EConstr.of_constr typ in let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in Some (tac, dep, succ (List.length ctx), vars) @@ -3797,7 +3787,6 @@ let specialize_eqs id gl = let open Context.Rel.Declaration in let env = Tacmach.pf_env gl in let ty = Tacmach.pf_get_hyp_typ gl id in - let ty = EConstr.of_constr ty in let evars = ref (project gl) in let unif env evars c1 c2 = compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 @@ -4062,7 +4051,6 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info = let guess_elim isrec dep s hyp0 gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in - let tmptyp0 = EConstr.of_constr tmptyp0 in let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in let evd, elimc = if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl @@ -4080,16 +4068,13 @@ let guess_elim isrec dep s hyp0 gl = (Sigma.to_evar_map sigma, ind) in let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - let elimt = EConstr.of_constr elimt in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in - let tmptyp0 = EConstr.of_constr tmptyp0 in let ind_type_guess,_ = decompose_app sigma (snd (decompose_prod sigma tmptyp0)) in let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - let elimt = EConstr.of_constr elimt in Tacmach.New.project gl, (e, elimt), ind_type_guess type scheme_signature = @@ -4127,7 +4112,7 @@ let get_elim_signature elim hyp0 gl = let is_functional_induction elimc gl = let sigma = Tacmach.New.project gl in - let scheme = compute_elim_sig sigma ~elimc (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (fst elimc))) in + let scheme = compute_elim_sig sigma ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -4162,7 +4147,6 @@ let recolle_clenv i params args elimclause gl = arr in let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in (* parameters correspond to first elts of lid. *) - let pf_get_hyp_typ id gl = EConstr.of_constr (pf_get_hyp_typ id gl) in let clauses_params = List.map_i (fun i id -> mkVar id , pf_get_hyp_typ id gl, lindmv.(i)) 0 params in @@ -4523,7 +4507,7 @@ let induction_gen_l isrec with_evars elim names lc = let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in let x = - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar (Global.env()) (EConstr.Unsafe.to_constr (type_of c)) Anonymous in let id = new_fresh_id [] x gl in let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in @@ -4778,7 +4762,6 @@ let symmetry_in id = Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in - let ctype = EConstr.of_constr ctype in let sign,t = decompose_prod_assum sigma ctype in Proofview.tclORELSE begin @@ -4832,7 +4815,6 @@ let prove_transitivity hdcncl eq_kind t = let sigma = Tacmach.New.project gl in let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in - let typt = EConstr.of_constr typt in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) in diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 5f33ae834..5e686c41e 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -321,11 +321,12 @@ let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind (* This function tryies to get the [inductive] between a constr the constr should be Ind i or App(Ind i,[|args|]) *) -let destruct_ind c = - try let u,v = destApp c in - let indc = destInd u in +let destruct_ind sigma c = + let open EConstr in + try let u,v = destApp sigma c in + let indc = destInd sigma u in indc,v - with DestKO -> let indc = destInd c in + with DestKO -> let indc = destInd sigma c in indc,[||] (* @@ -338,11 +339,12 @@ so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) let do_replace_lb mode lb_scheme_key aavoid narg p q = + let open EConstr in let avoid = Array.of_list aavoid in - let do_arg v offset = + let do_arg sigma v offset = try let x = narg*offset in - let s = destVar v in + let s = destVar sigma v in let n = Array.length avoid in let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) @@ -355,7 +357,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (* if this happen then the args have to be already declared as a Parameter*) ( - let mp,dir,lbl = repr_con (fst (destConst v)) in + let mp,dir,lbl = repr_con (fst (destConst sigma v)) in mkConst (make_con mp dir (mk_label ( if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) else ((Label.to_string lbl)^"_lb") @@ -364,7 +366,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = in Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in - let u,v = destruct_ind type_of_pq + let sigma = Tacmach.New.project gl in + let u,v = destruct_ind sigma type_of_pq in let lb_type_of_p = try let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in @@ -376,20 +379,20 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (str "Leibniz->boolean:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_constr type_of_pq ++ + Printer.pr_econstr type_of_pq ++ str " first.") in Tacticals.New.tclZEROMSG err_msg in lb_type_of_p >>= fun (lb_type_of_p,eff) -> + Proofview.tclEVARMAP >>= fun sigma -> let lb_args = Array.append (Array.append (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg x 1) v)) - (Array.map (fun x -> do_arg x 2) v) - in let app = if Array.equal Term.eq_constr lb_args [||] + (Array.map (fun x -> do_arg sigma x 1) v)) + (Array.map (fun x -> do_arg sigma x 2) v) + in let app = if Array.is_empty lb_args then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in - let app = EConstr.of_constr app in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; Equality.replace p q ; apply app ; Auto.default_auto] @@ -397,13 +400,12 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = (* used in the bool -> leib side *) let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = - let lft = EConstr.Unsafe.to_constr lft in - let rgt = EConstr.Unsafe.to_constr rgt in + let open EConstr in let avoid = Array.of_list aavoid in - let do_arg v offset = + let do_arg sigma v offset = try let x = narg*offset in - let s = destVar v in + let s = destVar sigma v in let n = Array.length avoid in let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) @@ -416,7 +418,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = (* if this happen then the args have to be already declared as a Parameter*) ( - let mp,dir,lbl = repr_con (fst (destConst v)) in + let mp,dir,lbl = repr_con (fst (destConst sigma v)) in mkConst (make_con mp dir (mk_label ( if Int.equal offset 1 then ("eq_"^(Label.to_string lbl)) else ((Label.to_string lbl)^"_bl") @@ -427,13 +429,12 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec aux l1 l2 = match (l1,l2) with | (t1::q1,t2::q2) -> - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in Proofview.Goal.enter { enter = begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in - if EConstr.eq_constr (Tacmach.New.project gl) t1 t2 then aux q1 q2 + let sigma = Tacmach.New.project gl in + if EConstr.eq_constr sigma t1 t2 then aux q1 q2 else ( - let u,v = try destruct_ind tt1 + let u,v = try destruct_ind sigma tt1 (* trick so that the good sequence is returned*) with e when CErrors.noncritical e -> indu,[||] in if eq_ind (fst u) ind @@ -450,20 +451,19 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = (str "boolean->Leibniz:" ++ str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_constr tt1 ++ + Printer.pr_econstr tt1 ++ str " first.") in error err_msg in let bl_args = Array.append (Array.append (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg x 1) v)) - (Array.map (fun x -> do_arg x 2) v ) + (Array.map (fun x -> do_arg sigma x 1) v)) + (Array.map (fun x -> do_arg sigma x 2) v ) in - let app = if Array.equal Term.eq_constr bl_args [||] + let app = if Array.is_empty bl_args then bl_t1 else mkApp (bl_t1,bl_args) in - let app = EConstr.of_constr app in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; Equality.replace_by t1 t2 @@ -475,21 +475,22 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = | ([],[]) -> Proofview.tclUNIT () | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in - begin try Proofview.tclUNIT (destApp lft) + Proofview.tclEVARMAP >>= fun sigma -> + begin try Proofview.tclUNIT (destApp sigma lft) with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind1,ca1) -> - begin try Proofview.tclUNIT (destApp rgt) + begin try Proofview.tclUNIT (destApp sigma rgt) with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind2,ca2) -> - begin try Proofview.tclUNIT (out_punivs (destInd ind1)) + begin try Proofview.tclUNIT (out_punivs (destInd sigma ind1)) with DestKO -> - begin try Proofview.tclUNIT (fst (fst (destConstruct ind1))) + begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind1))) with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp1,i1) -> - begin try Proofview.tclUNIT (out_punivs (destInd ind2)) + begin try Proofview.tclUNIT (out_punivs (destInd sigma ind2)) with DestKO -> - begin try Proofview.tclUNIT (fst (fst (destConstruct ind2))) + begin try Proofview.tclUNIT (fst (fst (destConstruct sigma ind2))) with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp2,i2) -> diff --git a/toplevel/class.ml b/toplevel/class.ml index e55489471..4c7aa01cd 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -207,7 +207,7 @@ let build_id_coercion idf_opt source poly = let _ = if not (Reductionops.is_conv_leq env sigma - (EConstr.of_constr (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f))) (EConstr.of_constr typ_f)) + (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f)) (EConstr.of_constr typ_f)) then user_err (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/toplevel/classes.ml b/toplevel/classes.ml index acfbce357..5087aa0c8 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -83,7 +83,7 @@ let type_ctx_instance evars env ctx inst subst = let t' = substl subst (RelDecl.get_type decl) in let c', l = match decl with - | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l + | LocalAssum _ -> EConstr.Unsafe.to_constr (interp_casted_constr_evars env evars (List.hd l) t'), List.tl l | LocalDef (_,b,_) -> substl subst b, l in let d = RelDecl.get_name decl, Some c', t' in @@ -151,6 +151,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let k, u, cty, ctx', ctx, len, imps, subst = let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in let c', imps' = interp_type_evars_impls ~impls env' evars tclass in + let c' = EConstr.Unsafe.to_constr c' in let len = List.length ctx in let imps = imps @ Impargs.lift_implicits len imps' in let ctx', c = decompose_prod_assum c' in @@ -219,6 +220,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p | None -> if List.is_empty k.cl_props then Some (Inl subst) else None | Some (Inr term) -> let c = interp_casted_constr_evars env' evars term cty in + let c = EConstr.Unsafe.to_constr c in Some (Inr (c, subst)) | Some (Inl props) -> let get_id = diff --git a/toplevel/command.ml b/toplevel/command.ml index 1fc89b8b0..7e3828131 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -103,6 +103,7 @@ let interp_definition pl bl p red_option c ctypopt = let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in + let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Universes.universes_of_constr body in @@ -116,8 +117,10 @@ let interp_definition pl bl p red_option c ctypopt = let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in + let c = EConstr.Unsafe.to_constr c in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in + let ty = EConstr.Unsafe.to_constr ty in let typ = nf (Term.it_mkProd_or_LetIn ty ctx) in let beq b1 b2 = if b1 then b2 else not b2 in let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in @@ -264,6 +267,7 @@ match local with let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in let ty, impls = interp_type_evars_impls env evdref ~impls c in + let ty = EConstr.Unsafe.to_constr ty in let evd, nf = nf_evars_and_universes !evdref in let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) @@ -318,6 +322,7 @@ let do_assumptions_bound_univs coe kind nl id pl c = let evdref = ref (Evd.from_ctx ctx) in let ty, impls = interp_type_evars_impls env evdref c in let nf, subst = Evarutil.e_nf_evars_and_universes evdref in + let ty = EConstr.Unsafe.to_constr ty in let ty = nf ty in let vars = Universes.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in @@ -439,9 +444,10 @@ let interp_ind_arity env evdref ind = let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in let pseudo_poly = check_anonymous_type c in - let () = if not (Reduction.is_arity env t) then + let () = if not (Reductionops.is_arity env !evdref t) then user_err ~loc:(constr_loc ind.ind_arity) (str "Not an arity") in + let t = EConstr.Unsafe.to_constr t in t, pseudo_poly, impls let interp_cstrs evdref env impls mldata arity ind = @@ -449,7 +455,7 @@ let interp_cstrs evdref env impls mldata arity ind = (* Complete conclusions of constructor types if given in ML-style syntax *) let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in (* Interpret the constructor types *) - let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls) ctyps') in + let ctyps'', cimpls = List.split (List.map (interp_type_evars_impls evdref env ~impls %> on_fst EConstr.Unsafe.to_constr) ctyps') in (cnames, ctyps'', cimpls) let sign_level env evd sign = @@ -842,12 +848,14 @@ let interp_fix_context env evdref isfix fix = ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl evdref impls (env,_) fix = - interp_type_evars_impls ~impls env evdref fix.fix_type + let (c, impl) = interp_type_evars_impls ~impls env evdref fix.fix_type in + (EConstr.Unsafe.to_constr c, impl) let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = Option.map (fun body -> let env = push_rel_context ctx env_rec in let body = interp_casted_constr_evars env evdref ~impls body ccl in + let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body ctx) fix.fix_body let build_fix_type (_,ctx) ccl = Term.it_mkProd_or_LetIn ccl ctx @@ -946,6 +954,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let len = List.length binders_rel in let top_env = push_rel_context binders_rel env in let top_arity = interp_type_evars top_env evdref arityc in + let top_arity = EConstr.Unsafe.to_constr top_arity in let full_arity = Term.it_mkProd_or_LetIn top_arity binders_rel in let argtyp, letbinders, make = telescope binders_rel in let argname = Id.of_string "recarg" in @@ -953,22 +962,24 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let relty = Typing.unsafe_type_of env !evdref (EConstr.of_constr rel) in + let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = user_err ~loc:(constr_loc r) ~hdr:"Command.build_wellfounded" - (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") + (Printer.pr_econstr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try - let ctx, ar = Reductionops.splay_prod_n env !evdref 2 (EConstr.of_constr relty) in + let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in match ctx, EConstr.kind !evdref ar with | [LocalAssum (_,t); LocalAssum (_,u)], Sort (Prop Null) when Reductionops.is_conv env !evdref (EConstr.of_constr t) (EConstr.of_constr u) -> t | _, _ -> error () with e when CErrors.noncritical e -> error () in + let rel = EConstr.Unsafe.to_constr rel in let measure = interp_casted_constr_evars binders_env evdref measure relargty in + let measure = EConstr.Unsafe.to_constr measure in let wf_rel, wf_rel_fun, measure_fn = let measure_body, measure = it_mkLambda_or_LetIn measure letbinders, @@ -1025,6 +1036,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = interp_casted_constr_evars (push_rel_context ctx env) evdref ~impls:newimpls body (lift 1 top_arity) in + let intern_body = EConstr.Unsafe.to_constr intern_body in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in let def = @@ -1035,6 +1047,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = prop |]) in let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in + let def = EConstr.Unsafe.to_constr def in let _ = evdref := Evarutil.nf_evar_map !evdref in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context !evdref binders_rel in @@ -1110,7 +1123,7 @@ let interp_recursive isfix fixl notations = let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in - Typing.e_solve_evars env evdref (EConstr.of_constr app) + EConstr.Unsafe.to_constr (Typing.e_solve_evars env evdref (EConstr.of_constr app)) with e when CErrors.noncritical e -> t in LocalAssum (id,fixprot) :: env' diff --git a/toplevel/record.ml b/toplevel/record.ml index 73035deb0..a65f5252e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -66,7 +66,8 @@ let interp_fields_evars env evars impls_env nots l = List.fold_left2 (fun (env, uimpls, params, impls) no ((loc, i), b, t) -> let t', impl = interp_type_evars_impls env evars ~impls t in - let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in + let b' = Option.map (fun x -> EConstr.Unsafe.to_constr (fst (interp_casted_constr_evars_impls env evars ~impls x t'))) b in + let t' = EConstr.Unsafe.to_constr t' in let impls = match i with | Anonymous -> impls @@ -120,7 +121,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = match t with | CSort (_, Misctypes.GType []) -> true | _ -> false in let s = interp_type_evars env evars ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env !evars (EConstr.of_constr s) in + let sred = Reductionops.whd_all env !evars s in + let s = EConstr.Unsafe.to_constr s in let sred = EConstr.Unsafe.to_constr sred in (match kind_of_term sred with | Sort s' -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ee2aacfc5..4376f51dc 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -108,7 +108,7 @@ let show_intro all = let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in - let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (EConstr.of_constr (pf_concl gl))) in + let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) @@ -1572,6 +1572,7 @@ let get_current_context_of_args = function let vernac_check_may_eval redexp glopt rc = let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in + let c = EConstr.Unsafe.to_constr c in let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in |