diff options
41 files changed, 122 insertions, 181 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 138400991..bf8481b52 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -301,7 +301,6 @@ let project_hint pri l2r r = let sigma, c = Evd.fresh_global env sigma gr in let c = EConstr.of_constr c in let t = Retyping.get_type_of env sigma c in - let t = EConstr.of_constr t in let t = Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in let sign,ccl = decompose_prod_assum sigma t in @@ -667,7 +666,6 @@ let hResolve id c occ t = let t_constr = EConstr.of_constr t_constr in let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in - let t_constr_type = EConstr.of_constr t_constr_type in let tac = (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) in diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index a7ff8e142..85c19fac4 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -454,7 +454,7 @@ module TypeGlobal = struct end let sort_of_rel env evm rel = - Reductionops.sort_of_arity env evm (EConstr.of_constr (Retyping.get_type_of env evm rel)) + Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel) let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation @@ -524,14 +524,12 @@ let rec decompose_app_rel env evd t = let decompose_app_rel env evd t = let (rel, t1, t2) = decompose_app_rel env evd t in let ty = Retyping.get_type_of env evd rel in - let ty = EConstr.of_constr ty in let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in (rel, t1, t2) let decompose_applied_relation env sigma (c,l) = let open Context.Rel.Declaration in let ctype = Retyping.get_type_of env sigma c in - let ctype = EConstr.of_constr ctype in let find_rel ty = let sigma, cl = Clenv.make_evar_clause env sigma ty in let sigma = Clenv.solve_evar_clause env sigma true cl l in @@ -539,8 +537,6 @@ let decompose_applied_relation env sigma (c,l) = let (equiv, c1, c2) = decompose_app_rel env sigma t in let ty1 = Retyping.get_type_of env sigma c1 in let ty2 = Retyping.get_type_of env sigma c2 in - let ty1 = EConstr.of_constr ty1 in - let ty2 = EConstr.of_constr ty2 in match evd_convertible env sigma ty1 ty2 with | None -> None | Some sigma -> @@ -750,8 +746,6 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) and prf = nf prf in let ty1 = Retyping.get_type_of env evd c1 in let ty2 = Retyping.get_type_of env evd c2 in - let ty1 = EConstr.of_constr ty1 in - let ty2 = EConstr.of_constr ty2 in let () = if not (convertible env evd ty2 ty1) then raise Reduction.NotConvertible in let rew_evars = evd, cstrs in let rew_prf = RewPrf (rel, prf) in @@ -956,7 +950,6 @@ let reset_env env = let fold_match ?(force=false) env sigma c = let (ci, p, c, brs) = destCase sigma c in let cty = Retyping.get_type_of env sigma c in - let cty = EConstr.of_constr cty in let dep, pred, exists, (sk,eff) = let env', ctx, body = let ctx, pred = decompose_lam_assum sigma p in @@ -1020,7 +1013,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = state, (None :: acc, evars, progress) else let argty = Retyping.get_type_of env (goalevars evars) arg in - let argty = EConstr.of_constr argty in let state, res = s.strategy { state ; env ; unfresh ; term1 = arg ; ty1 = argty ; @@ -1069,7 +1061,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in if flags.on_morphisms then let mty = Retyping.get_type_of env (goalevars evars) m in - let mty = EConstr.of_constr mty in let evars, cstr', m, mty, argsl, args = let argsl = Array.to_list args in let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in @@ -1113,8 +1104,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let b = subst1 mkProp b in let tx = Retyping.get_type_of env (goalevars evars) x and tb = Retyping.get_type_of env (goalevars evars) b in - let tx = EConstr.of_constr tx in - let tb = EConstr.of_constr tb in let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in @@ -1193,7 +1182,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let open Context.Rel.Declaration in let env' = Environ.push_rel (local_assum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in - let bty = EConstr.of_constr bty in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in let state, b' = s.strategy { state ; env = env' ; unfresh ; term1 = b ; ty1 = bty ; @@ -1221,7 +1209,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Case (ci, p, c, brs) -> let cty = Retyping.get_type_of env (goalevars evars) c in - let cty = EConstr.of_constr cty in let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in let cstr' = Some eqty in let state, c' = s.strategy { state ; env ; unfresh ; @@ -1500,7 +1487,6 @@ let rewrite_with l2r flags c occs : strategy = { strategy = let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars = let ty = Retyping.get_type_of env (goalevars evars) concl in - let ty = EConstr.of_constr ty in let _, res = s.strategy { state = () ; env ; unfresh ; term1 = concl ; ty1 = ty ; cstr = (prop, Some cstr) ; evars } in @@ -1917,10 +1903,8 @@ let declare_projection n instance_id r = let sigma,c = Evd.fresh_global env sigma r in let c = EConstr.of_constr c in let ty = Retyping.get_type_of env sigma c in - let ty = EConstr.of_constr ty in let term = proper_projection sigma c ty in let sigma, typ = Typing.type_of env sigma term in - let typ = EConstr.of_constr typ in let ctx, typ = decompose_prod_assum sigma typ in let typ = let n = @@ -2115,7 +2099,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = and car = nf car and rel = nf rel in check_evar_map_of_evars_defs sigma; let prf = nf prf in - let prfty = nf (EConstr.of_constr (Retyping.get_type_of env sigma prf)) in + let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in let abs = prf, prfty in let prf = mkRel 1 in @@ -2183,7 +2167,6 @@ let setoid_proof ty fn fallback = try let rel, _, _ = decompose_app_rel env sigma concl in let (sigma, t) = Typing.type_of env sigma rel in - let t = EConstr.of_constr t in let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 6c59abe66..b4d2b1e50 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -802,7 +802,8 @@ let interp_may_eval f ist env sigma = function (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) + let (sigma, t) = Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) in + (sigma, EConstr.Unsafe.to_constr t) | ConstrTerm c -> try f ist env sigma c diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7a99c45a8..a4ed4798a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -264,7 +264,6 @@ let refresh_universes ty k = let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in let evm, ty = refresh_type env evm ty in - let ty = EConstr.of_constr ty in Sigma.Unsafe.of_pair (k ty, evm) end } @@ -387,7 +386,6 @@ let discriminate_tac (cstr,u as cstru) p = 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 intype = EConstr.of_constr intype 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 @@ -496,9 +494,7 @@ let mk_eq f c1 c2 k = Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in - let ty = EConstr.of_constr ty in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in - let ty = EConstr.of_constr ty in let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 61547f96d..7b7e746f2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,7 +42,7 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))) let sort_of env c = let polyprop = (lang() == Haskell) in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cc29d68f5..c98cdc467 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -985,6 +985,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in + let t = EConstr.Unsafe.to_constr t in decompose_prod_n_assum (nb_params + nb_args) t,evd in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 38cd21684..0725bb11c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1273,6 +1273,7 @@ let do_build_inductive Array.fold_right2 (fun id c (evd,env) -> let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in + let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 37a76bec1..1b899c152 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -373,6 +373,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in + let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca066c4cc..27528c2dc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -135,6 +135,7 @@ let generate_type evd g_to_f f graph i = in evd:=evd'; let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in + let graph_arity = EConstr.Unsafe.to_constr graph_arity in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -203,6 +204,7 @@ let find_induction_principle evd f = | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in + let typ = EConstr.Unsafe.to_constr typ in evd:=evd'; rect_lemma,typ diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f96b189c5..ced572466 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -898,7 +898,7 @@ struct let has_typ gl t1 typ = let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in - Constr.equal ty typ + EConstr.eq_constr (Tacmach.project gl) ty (EConstr.of_constr typ) let is_convertible gl t1 t2 = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 131ecad33..c0eeff8d7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -344,6 +344,8 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) +let pr_constr c = pr_constr (EConstr.Unsafe.to_constr c) + module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -357,12 +359,12 @@ let find_ring_structure env sigma l = let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then + if not (Reductionops.is_conv env sigma ty ty') then user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; - (try ring_for_carrier ty + (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ @@ -495,7 +497,6 @@ let op_smorph r add mul req m1 m2 = (* (setoid,op_morph) *) let ring_equality env evd (r,add,mul,opp,req) = - let pr_constr c = pr_constr (EConstr.to_constr !evd c) in match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> let setoid = plapp evd coq_eq_setoid [|r|] in @@ -553,7 +554,6 @@ let build_setoid_params env evd r add mul opp req eqth = let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in - let th_typ = EConstr.of_constr th_typ in match EConstr.kind sigma th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) when eq_constr_nounivs sigma f (Lazy.force coq_almost_ring_theory) -> @@ -585,7 +585,6 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in - let t = EConstr.of_constr t in plapp evd coq_mkhypo [|t;c|] let make_hyp_list env evd lH = @@ -820,7 +819,6 @@ let sf_sr = my_reference"SF_SR" let dest_field env evd th_spec = let open Termops in let th_typ = Retyping.get_type_of env !evd th_spec in - let th_typ = EConstr.of_constr th_typ in match EConstr.kind !evd th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) when is_global !evd (Lazy.force afield_theory) f -> @@ -852,12 +850,12 @@ let find_field_structure env sigma l = let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then + if not (Reductionops.is_conv env sigma ty ty') then user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; - (try field_for_carrier ty + (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> user_err ~hdr:"field" (str"cannot find a declared field structure over"++ diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d34c9325e..9798fa11c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1390,9 +1390,10 @@ let ssrpatterntac _ist (arg_ist,arg) gl = let concl0 = pf_concl gl in let (t, uc), concl_x = fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in - let gl, tty = pf_type_of gl (EConstr.of_constr t) in - let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in - let concl = EConstr.of_constr concl in + let t = EConstr.of_constr t in + let concl_x = EConstr.of_constr concl_x in + let gl, tty = pf_type_of gl t in + let concl = EConstr.mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 01e2db08c..565a9725c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1502,7 +1502,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then (* Try to compile first using non expanded alias *) try - if initial then f orig (EConstr.of_constr (Retyping.get_type_of pb.env sigma orig)) + if initial then f orig (Retyping.get_type_of pb.env sigma orig) else just_pop () with e when precatchable_exception e -> (* Try then to compile using expanded alias *) @@ -1517,7 +1517,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = (* Could be needed in case of a recursive call which requires to be on a variable for size reasons *) pb.evdref := sigma; - if initial then f orig (EConstr.of_constr (Retyping.get_type_of pb.env !(pb.evdref) orig)) + if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) else just_pop () @@ -1650,13 +1650,12 @@ let abstract_tycon loc env evdref subst tycon extenv t = | Rel n when is_local_def (lookup_rel n env) -> t | Evar ev -> let ty = get_type_of env !evdref t in - let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref (EConstr.of_constr ty) in + let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let inst = List.map_i (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ty = EConstr.of_constr ty in let ev' = e_new_evar env evdref ~src ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd @@ -1672,10 +1671,8 @@ let abstract_tycon loc env evdref subst tycon extenv t = let vl = List.map pi1 good in let ty = let ty = get_type_of env !evdref t in - let ty = EConstr.of_constr ty in Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in - let ty = EConstr.of_constr ty in let ty = lift (-k) (aux x ty) in let depvl = free_rels !evdref ty in let inst = @@ -1708,7 +1705,6 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in let evd,tt = Typing.type_of extenv !evdref t in - let tt = EConstr.of_constr tt in evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in @@ -2109,7 +2105,6 @@ let constr_of_pat env evdref arsign pat avoid = let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in let apptype = Retyping.get_type_of env ( !evdref) app in - let apptype = EConstr.of_constr apptype in let IndType (indf, realargs) = find_rectype env (!evdref) apptype in match alias with Anonymous -> @@ -2370,7 +2365,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign = let t = RelDecl.get_type decl in let t = EConstr.of_constr t in let argt = Retyping.get_type_of env !evdref arg in - let argt = EConstr.of_constr argt in let eq, refl_arg = if Reductionops.is_conv env !evdref argt t then (mk_eq evdref (lift (nargeqs + slift) argt) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index e4331aade..13310c44d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -442,6 +442,7 @@ let cache_coercion (_, c) = let it, _ = class_info c.coercion_target in let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; coe_type = typ; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7e8559630..f569d9fc4 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -66,7 +66,7 @@ let apply_coercion_args env evd check isproj argl funj = | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) match EConstr.kind !evdref (whd_all env !evdref typ) with | Prod (_,c1,c2) -> - if check && not (e_cumul env evdref (EConstr.of_constr (Retyping.get_type_of env !evdref h)) c1) then + if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl | _ -> anomaly (Pp.str "apply_coercion_args") @@ -498,7 +498,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in let t2 = match v2 with | None -> subst_term evd' v1 t2 - | Some v2 -> EConstr.of_constr (Retyping.get_type_of env1 evd' v2) in + | Some v2 -> Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 3d5a5f025..d4e156fa4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -504,7 +504,7 @@ let rec detype flags avoid env sigma t = let pb = Environ.lookup_projection p (snd env) in let body = pb.Declarations.proj_body in let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in - let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma (EConstr.of_constr ty) in + let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let args = List.map EConstr.Unsafe.to_constr args in let body' = strip_lam_assum body in let body' = subst_instance_constr u body' in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6dce8627d..afb0bf6d5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -168,7 +168,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = - try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) + try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 | None -> @@ -882,7 +882,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) List.fold_left (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then - let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in + let ty = Retyping.get_type_of env i t2 in let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else @@ -1052,7 +1052,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let id = NamedDecl.get_id decl' in let t = EConstr.of_constr (NamedDecl.get_type decl') in let evs = ref [] in - let ty = EConstr.of_constr (Retyping.get_type_of env_rhs evd c) in + let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3003620d7..de2e46a78 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -23,6 +23,14 @@ open Evarutil open Pretype_errors open Sigma.Notations +let nlocal_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + Context.Named.Declaration.LocalAssum (na, inj t) + +let nlocal_def (na, b, t) = + let inj = EConstr.Unsafe.to_constr in + Context.Named.Declaration.LocalDef (na, inj b, inj t) + let normalize_evar evd ev = match EConstr.kind evd (mkEvar ev) with | Evar (evk,args) -> (evk,args) @@ -108,11 +116,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) | Some dir -> refresh status dir t) else (refresh_term_evars false true t; t) in - if !modified then !evdref, EConstr.Unsafe.to_constr t' else !evdref, EConstr.Unsafe.to_constr t + if !modified then !evdref, t' else !evdref, t let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in - refresh_universes (Some false) env sigma (EConstr.of_constr ty) + refresh_universes (Some false) env sigma ty (************************) @@ -146,7 +154,7 @@ let recheck_applications conv_algo env evdref t = | App (f, args) -> let () = aux env f in let fty = Retyping.get_type_of env !evdref f in - let argsty = Array.map (fun x -> aux env x; EConstr.of_constr (Retyping.get_type_of env !evdref x)) args in + let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in let rec aux i ty = if i < Array.length argsty then match EConstr.kind !evdref (whd_all env !evdref ty) with @@ -158,7 +166,7 @@ let recheck_applications conv_algo env evdref t = Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) else () - in aux 0 (EConstr.of_constr fty) + in aux 0 fty | _ -> iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t in aux env t @@ -173,7 +181,7 @@ type 'a update = | NoUpdate open Context.Named.Declaration -let inst_of_vars sign = Array.map_of_list (get_id %> EConstr.mkVar) sign +let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign let restrict_evar_key evd evk filter candidates = match filter, candidates with @@ -413,9 +421,9 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c = let rec expand_and_check_vars sigma aliases = function | [] -> [] - | a::l when EConstr.isRel sigma a || EConstr.isVar sigma a -> + | a::l when isRel sigma a || isVar sigma a -> let a = expansion_of_var sigma aliases a in - if EConstr.isRel sigma a || EConstr.isVar sigma a then a :: expand_and_check_vars sigma aliases l + if isRel sigma a || isVar sigma a then a :: expand_and_check_vars sigma aliases l else raise Exit | _ -> raise Exit @@ -480,7 +488,7 @@ let is_unification_pattern_meta env evd nb m l t = (* so we need to be a rel <= nb *) if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then match find_unification_pattern_args env evd l t with - | Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x + | Some _ as x when not (dependent evd (mkMeta m) t) -> x | _ -> None else None @@ -591,15 +599,15 @@ let make_projectable_subst aliases sigma evi args = let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env = let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src inst_in_env in + let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in let evd = Sigma.to_evar_map evd in let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in let (evk, _) = destEvar evd evar_in_env in - let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in + let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in let ctxt = named_context_of_val sign in let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in let evar_in_sign = mkEvar (evk, inst_in_sign) in - (evd,whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign)) + (evd,EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr evar_in_sign))) (* We have x1..xq |- ?e1 : τ and had to solve something like * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some @@ -624,7 +632,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = if Evd.is_defined evd evk1 then (* Some circularity somewhere (see e.g. #3209) *) raise MorePreciseOccurCheckNeeeded; - let (evk1,args1) = EConstr.destEvar evd (EConstr.mkEvar (evk1,args1)) in + let (evk1,args1) = destEvar evd (mkEvar (evk1,args1)) in let evi1 = Evd.find_undefined evd evk1 in let env1,rel_sign = env_rel_context_chop k env in let sign1 = evar_hyps evi1 in @@ -641,16 +649,16 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let t_in_env = EConstr.of_constr t_in_env in let s = Retyping.get_sort_of env evd t_in_env in let evd,ty_t_in_sign = refresh_universes - ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in + ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env in let evd,d' = match d with - | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign) + | LocalAssum _ -> evd, nlocal_assum (id,t_in_sign) | LocalDef (_,b,_) -> let b = EConstr.of_constr b in let evd,b = define_evar_from_virtual_equation define_fun env evd src b t_in_sign sign filter inst_in_env in - evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in + evd, nlocal_def (id,b,t_in_sign) in (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), @@ -661,11 +669,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in let evd,ty_t_in_sign = refresh_universes - ~status:univ_flexible (Some false) env evd (EConstr.mkSort s) in + ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let evd = Sigma.Unsafe.of_evar_map evd in - let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in let Sigma (ev2_in_sign, evd, _) = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in let evd = Sigma.to_evar_map evd in @@ -899,7 +906,7 @@ let extract_unique_projection = function let extract_candidates sols = try UpdateWith - (List.map (function (id,ProjectVar) -> EConstr.mkVar id | _ -> raise Exit) sols) + (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols) with Exit -> NoUpdate @@ -1171,7 +1178,7 @@ let check_evar_instance evd evk1 body conv_algo = (* FIXME: The body might be ill-typed when this is called from w_merge *) (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = - try EConstr.of_constr (Retyping.get_type_of ~lax:true evenv evd body) + try Retyping.get_type_of ~lax:true evenv evd body with Retyping.RetypeError _ -> error "Ill-typed evar instance" in match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with @@ -1378,7 +1385,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | (id,p)::_::_ -> if choose then (mkVar id, p) else raise (NotUniqueInType sols) in - let ty = lazy (EConstr.of_constr (Retyping.get_type_of env !evdref t)) in + let ty = lazy (Retyping.get_type_of env !evdref t) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in evdref := evd; c @@ -1440,7 +1447,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = if not !progress then raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) - let ty = EConstr.of_constr (get_type_of env' evd t) in + let ty = get_type_of env' evd t in let (evd,evar'',ev'') = materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) @@ -1474,7 +1481,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | _ -> None with | Some l -> - let ty = EConstr.of_constr (get_type_of env' !evdref t) in + let ty = get_type_of env' !evdref t in let candidates = try let t = @@ -1563,15 +1570,15 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) - let evd' = check_evar_instance evd' evk (EConstr.of_constr body) conv_algo in - Evd.define evk body evd' + let evd' = check_evar_instance evd' evk body conv_algo in + Evd.define evk (EConstr.Unsafe.to_constr body) evd' with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs | NotEnoughInformationEvarEvar t -> - add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,t) evd + add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd | MorePreciseOccurCheckNeeeded -> - add_conv_oriented_pb (pbty,env,EConstr.mkEvar ev,rhs) evd + add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> raise e | OccurCheckIn (evd,rhs) -> diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index b83147514..f2102f8cd 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -42,7 +42,7 @@ val refresh_universes : (* Also refresh Prop and Set universes, so that the returned type can be any supertype of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> - env -> evar_map -> types -> evar_map * Constr.types + env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> bool option -> existential_key -> constr array -> constr array -> evar_map @@ -77,4 +77,4 @@ val remove_instance_local_defs : evar_map -> existential_key -> 'a array -> 'a list val get_type_of_refresh : - ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * Constr.types + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7d2c96bb9..a0d8faab4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -426,7 +426,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c) + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> user_err (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++ @@ -774,9 +774,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre refreshed right away. *) let c = mkApp (f, args) in let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in - let c = EConstr.of_constr c in let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in - let t = EConstr.of_constr t in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -840,7 +838,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in - let t = EConstr.of_constr t in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) @@ -1025,7 +1022,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref tj.utj_val in - let tval = EConstr.of_constr tval in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> @@ -1097,7 +1093,6 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - let t = EConstr.of_constr t in match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 7db30bf23..a9529d560 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -109,7 +109,7 @@ let retype ?(polyprop=true) sigma = lift n ty | Var id -> type_of_var env id | Const cst -> EConstr.of_constr (rename_type_of_constant env cst) - | Evar (evk, args) -> EConstr.of_constr (Evd.existential_type sigma (evk, Array.map EConstr.Unsafe.to_constr args)) + | Evar ev -> existential_type sigma ev | Ind ind -> EConstr.of_constr (rename_type_of_inductive env ind) | Construct cstr -> EConstr.of_constr (rename_type_of_constructor env cstr) | Case (_,p,c,lf) -> @@ -210,7 +210,7 @@ let get_sort_of ?(polyprop=true) env sigma t = let get_sort_family_of ?(polyprop=true) env sigma c = let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in EConstr.Unsafe.to_constr (anomaly_on_error (f env c) args) + let _,_,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with @@ -238,10 +238,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = let f,_,_,_ = retype ~polyprop sigma in - if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c) + if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) -let get_judgment_of env evc c = { uj_val = c; uj_type = EConstr.of_constr (get_type_of env evc c) } +let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c } (* Returns sorts of a context *) let sorts_of_context env evc ctxt = @@ -256,7 +256,7 @@ let sorts_of_context env evc ctxt = let expand_projection env sigma pr c args = let ty = get_type_of ~lax:true env sigma c in let (i,u), ind_args = - try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) + try Inductiveops.find_mrectype env sigma ty with Not_found -> retype_error BadRecursiveType in mkApp (mkConstU (Projection.constant pr,u), diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index a20b11b76..ce9e1635f 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -9,6 +9,7 @@ open Term open Evd open Environ +open EConstr (** This family of functions assumes its constr argument is known to be well-typable. It does not type-check, just recompute the type @@ -26,25 +27,25 @@ type retype_error exception RetypeError of retype_error val get_type_of : - ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> types + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types val get_sort_of : - ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts + ?polyprop:bool -> env -> evar_map -> types -> sorts val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family + ?polyprop:bool -> env -> evar_map -> types -> sorts_family (** Makes an unsafe judgment from a constr *) -val get_judgment_of : env -> evar_map -> EConstr.constr -> EConstr.unsafe_judgment +val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment -val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr -> - EConstr.constr array -> types +val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> + constr array -> types val type_of_global_reference_knowing_conclusion : - env -> evar_map -> EConstr.constr -> EConstr.types -> evar_map * EConstr.types + env -> evar_map -> constr -> types -> evar_map * types val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list -val expand_projection : env -> evar_map -> Names.projection -> EConstr.constr -> EConstr.constr list -> EConstr.constr +val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.std_ppcmds diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 02524f896..3fc01c86c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1148,7 +1148,6 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in - let ta = EConstr.of_constr ta in let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in if occur_meta sigma ta then error "Cannot find a type for the generalisation."; if occur_meta sigma a then diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9ee34341b..9da7005e0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -270,7 +270,7 @@ let add_class cl = let check_instance env sigma c = try let (evd, c) = resolve_one_typeclass env sigma - (EConstr.of_constr (Retyping.get_type_of env sigma c)) in + (Retyping.get_type_of env sigma c) in not (Evd.has_undefined evd) with e when CErrors.noncritical e -> false @@ -314,7 +314,7 @@ let build_subclasses ~check env sigma glob pri = let declare_proj hints (cref, pri, body) = let path' = cref :: path in let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in - let rest = aux pri body (EConstr.of_constr ty) path' in + let rest = aux pri body ty path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index f67e0bddc..d24160ea5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -395,7 +395,7 @@ let type_of ?(refresh=false) env evd c = (* side-effect on evdref *) if refresh then Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type - else !evdref, EConstr.Unsafe.to_constr j.uj_type + else !evdref, j.uj_type let e_type_of ?(refresh=false) env evdref c = let env = enrich_env env evdref in @@ -405,7 +405,7 @@ let e_type_of ?(refresh=false) env evdref c = let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in let () = evdref := evd in c - else EConstr.Unsafe.to_constr j.uj_type + else j.uj_type let e_solve_evars env evdref c = let env = enrich_env env evdref in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 94a56b6e1..bf26358a2 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -19,10 +19,10 @@ val unsafe_type_of : env -> evar_map -> EConstr.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 * types +val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * EConstr.types (** Variant of [type_of] using references instead of state-passing. *) -val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> types +val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> EConstr.types (** Typecheck a type and return its sort *) val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8a8649f11..233b58e91 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -122,7 +122,6 @@ let abstract_list_all env evd typ c l = error_cannot_find_well_typed_abstraction env evd p l None | Pretype_errors.PretypeError (env',evd,TypingError x) -> error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in - let typp = EConstr.of_constr typp in evd,(p,typp) let set_occurrences_of_last_arg args = @@ -704,7 +703,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e (try let tyM = Typing.meta_type sigma k in let tyN = get_type_of curenv ~lax:true sigma cN in - let tyN = EConstr.of_constr tyN in check_compatibility curenv CUMUL flags substn tyN tyM with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma) @@ -724,7 +722,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if opt.with_types && flags.check_applied_meta_types then (try let tyM = get_type_of curenv ~lax:true sigma cM in - let tyM = EConstr.of_constr tyM in let tyN = Typing.meta_type sigma k in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> @@ -911,8 +908,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e try (* Force unification of the types to fill in parameters *) let ty1 = get_type_of curenv ~lax:true sigma c1 in let ty2 = get_type_of curenv ~lax:true sigma c2 in - let ty1 = EConstr.of_constr ty1 in - let ty2 = EConstr.of_constr ty2 in unify_0_with_initial_metas substn true curenv cv_pb { flags with modulo_conv_on_closed_terms = Some full_transparent_state; modulo_delta = full_transparent_state; @@ -978,8 +973,6 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e try (* Ensure we call conversion on terms of the same type *) let tyM = get_type_of curenv ~lax:true sigma m1 in let tyN = get_type_of curenv ~lax:true sigma n1 in - let tyM = EConstr.of_constr tyM in - let tyN = EConstr.of_constr tyN in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma @@ -1267,13 +1260,11 @@ let w_coerce_to_type env evd c cty mvty = let w_coerce env evd mv c = let cty = get_type_of env evd c in let mvty = Typing.meta_type evd mv in - w_coerce_to_type env evd c (EConstr.of_constr cty) mvty + w_coerce_to_type env evd c cty mvty let unify_to_type env sigma flags c status u = let sigma, c = refresh_universes (Some false) env sigma c in - let c = EConstr.of_constr c in let t = get_type_of env sigma (nf_meta sigma c) in - let t = EConstr.of_constr t in let t = nf_betaiota sigma (nf_meta sigma t) in unify_0 env sigma CUMUL flags t u @@ -1406,7 +1397,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = let evd' = Sigma.to_evar_map evd' in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags - (EConstr.of_constr (get_type_of sp_env evd' c)) (EConstr.of_constr ev.evar_concl) in + (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' then Evd.define sp (EConstr.Unsafe.to_constr c) evd''' @@ -1458,13 +1449,13 @@ let check_types env flags (sigma,_,_ as subst) m n = if isEvar_or_Meta sigma (head_app sigma m) then unify_0_with_initial_metas subst true env CUMUL flags - (EConstr.of_constr (get_type_of env sigma n)) - (EConstr.of_constr (get_type_of env sigma m)) + (get_type_of env sigma n) + (get_type_of env sigma m) else if isEvar_or_Meta sigma (head_app sigma n) then unify_0_with_initial_metas subst true env CUMUL flags - (EConstr.of_constr (get_type_of env sigma m)) - (EConstr.of_constr (get_type_of env sigma n)) + (get_type_of env sigma m) + (get_type_of env sigma n) else subst let try_resolve_typeclasses env evd flag m n = @@ -1595,7 +1586,6 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = else t, [] in let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in let ty = Retyping.get_type_of env sigma t in - let ty = EConstr.of_constr ty in if not (is_correct_type ty) then raise (NotUnifiable None); Some(sigma, t, l2) with @@ -1628,8 +1618,8 @@ let make_eq_test env evd c = let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = - let ty = Option.map EConstr.Unsafe.to_constr ty in let t = match ty with Some t -> t | None -> get_type_of env sigma c in + let t = EConstr.Unsafe.to_constr t in let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a428ab0ed..393e958d3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -62,7 +62,7 @@ let refresh_undefined_univs clenv = let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t -let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c) +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause @@ -673,9 +673,7 @@ let evar_of_binder holes = function let define_with_type sigma env ev c = let open EConstr in let t = Retyping.get_type_of env sigma ev in - let t = EConstr.of_constr t in let ty = Retyping.get_type_of env sigma c in - let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in let (ev, _) = destEvar sigma ev in diff --git a/proofs/logic.ml b/proofs/logic.ml index 98ad9ebe3..8b890f6f8 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -331,7 +331,7 @@ let meta_free_prefix sigma a = let goal_type_of env sigma c = if !check then unsafe_type_of env sigma (EConstr.of_constr c) - else Retyping.get_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 = let env = Goal.V82.env sigma goal in @@ -341,6 +341,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = in if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in + let t'ty = EConstr.Unsafe.to_constr t'ty in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else @@ -377,6 +378,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) in + let ty = EConstr.Unsafe.to_constr ty in goalacc, ty, sigma, f else mk_hdgoals sigma goal goalacc f @@ -390,6 +392,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> @@ -439,7 +442,7 @@ and mk_hdgoals sigma goal goalacc trm = if is_template_polymorphic env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in - (goalacc,type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l',sigma,f) + (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in @@ -465,6 +468,7 @@ and mk_hdgoals sigma goal goalacc trm = let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | _ -> diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index a830e25d9..8878051c8 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = let ctyp = Retyping.get_type_of env sigma c in - Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) + Vnorm.cbv_vm env sigma c ctyp let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -38,7 +38,7 @@ let cbv_native env sigma c = cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) + Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = diff --git a/proofs/refine.ml b/proofs/refine.ml index 32064aff5..c36bb143e 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -135,7 +135,6 @@ let refine ?(unsafe = true) f = let with_type env evd c t = let my_type = Retyping.get_type_of env evd c in - let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d9caadd54..7ffb30fa8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -108,7 +108,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls +let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c @@ -234,7 +234,7 @@ module New = struct let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) + pf_whd_all gl (pf_get_type_of gl t) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 06b3e3981..f0471bf66 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,7 +41,7 @@ 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 * 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_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t @@ -109,7 +109,7 @@ module New : sig val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.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 * 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_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b1d5d8135..2f8af6b44 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -283,7 +283,6 @@ let clenv_of_prods poly nprods (c, clenv) gl = else let sigma = Tacmach.New.project gl in let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in - let ty = EConstr.of_constr ty in let diff = nb_prod sigma ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) @@ -477,7 +476,6 @@ let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) let is_Prop env sigma concl = let ty = Retyping.get_type_of env sigma concl in - let ty = EConstr.of_constr ty in match EConstr.kind sigma ty with | Sort (Prop Null) -> true | _ -> false diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index e68267584..855273d3b 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -597,6 +597,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let fix_r2l_forward_rew_scheme (c, ctx') = let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in + let t = EConstr.Unsafe.to_constr t in let ctx,_ = decompose_prod_assum t in match ctx with | hp :: p :: ind :: indargs -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 494f36d7d..e1c39bb34 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -188,7 +188,6 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let instantiate_lemma gl c ty l l2r concl = let sigma, ct = pf_type_of gl c in - let ct = EConstr.of_constr ct in let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in [eqclause] @@ -452,7 +451,6 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in - let ctype = EConstr.of_constr ctype in let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in match match_with_equality_type sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) @@ -635,8 +633,6 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = let get_type_of = pf_apply get_type_of gl in let t1 = get_type_of c1 and t2 = get_type_of c2 in - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in let evd = if unsafe then Some (Tacmach.New.project gl) else @@ -733,7 +729,6 @@ let _ = let find_positions env sigma t1 t2 = let project env sorts posn t1 t2 = let ty1 = get_type_of env sigma t1 in - let ty1 = EConstr.of_constr ty1 in let s = get_sort_family_of env sigma ty1 in if Sorts.List.mem s sorts then [(List.rev posn,t1,t2)] else [] @@ -856,7 +851,7 @@ let injectable env sigma t1 t2 = let descend_then env sigma head dirn = let IndType (indf,_) = - try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head)) + try find_rectype env sigma (get_type_of env sigma head) with Not_found -> error "Cannot project on an inductive type derived from a dependency." in let indp,_ = (dest_ind_family indf) in @@ -912,7 +907,6 @@ let build_selector env sigma dirn c ind special default = let (indp,_) = dest_ind_family indf in let ind, _ = check_privacy env indp in let typ = Retyping.get_type_of env sigma default in - let typ = EConstr.of_constr typ in let (mib,mip) = lookup_mind_specif env ind in let deparsign = make_arity_signature env true indf in let p = it_mkLambda_or_LetIn typ deparsign in @@ -932,7 +926,6 @@ let build_coq_I () = EConstr.of_constr (build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> let ind = get_type_of env sigma c in - let ind = EConstr.of_constr ind in let true_0,false_0 = build_coq_True(),build_coq_False() in build_selector env sigma dirn c ind true_0 false_0 @@ -1108,7 +1101,6 @@ let make_tuple env sigma (rterm,rty) lind = assert (not (noccurn sigma lind rty)); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in - let a = EConstr.of_constr a in let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in @@ -1396,7 +1388,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let congr = EConstr.of_constr congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in let sigma, pf_typ = Typing.type_of env sigma pf in - let pf_typ = EConstr.of_constr pf_typ in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in let pf = Clenvtac.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in @@ -1567,7 +1558,6 @@ let lambda_create env (a,b) = let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let sigma = Sigma.to_evar_map sigma in let typ = get_type_of env sigma dep_pair1 in - let typ = EConstr.of_constr typ in (* We find all possible decompositions *) let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in @@ -1659,7 +1649,6 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None let substClause l2r c cls = Proofview.Goal.enter { enter = begin fun gl -> let eq = pf_apply get_type_of gl c in - let eq = EConstr.of_constr eq in tclTHENS (cutSubstClause l2r eq cls) [Proofview.tclUNIT (); exact_no_check c] end } diff --git a/tactics/hints.ml b/tactics/hints.ml index d4b73706c..9e9635e8a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -855,7 +855,6 @@ let fresh_global_or_constr env sigma poly cr = let make_resolves env sigma flags pri poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in - let cty = EConstr.of_constr cty in let try_apply f = try Some (f (c, cty, ctx)) with Failure _ -> None in let ents = List.map_filter try_apply diff --git a/tactics/inv.ml b/tactics/inv.ml index e45eb2a16..a398e04dd 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -63,10 +63,10 @@ let var_occurs_in_pf gl id = *) -type inversion_status = Dep of EConstr.constr option | NoDep +type inversion_status = Dep of constr option | NoDep let compute_eqn env sigma n i ai = - (mkRel (n-i),EConstr.of_constr (get_type_of env sigma (mkRel (n-i)))) + (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) let make_inv_predicate env evd indf realargs id status concl = let nrealargs = List.length realargs in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b2f2797a6..574f1c6f3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -818,13 +818,10 @@ let make_change_arg c pats = let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in - let t1 = EConstr.of_constr t1 in if deep then begin let t2 = Retyping.get_type_of env sigma origc in - let t2 = EConstr.of_constr t2 in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in - let t2 = EConstr.of_constr t2 in let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in if not b then if @@ -1448,7 +1445,6 @@ let general_elim_clause_gen elimtac indclause elim = let sigma = Tacmach.New.project gl in let (elimc,lbindelimc) = elim.elimbody in let elimt = Retyping.get_type_of env sigma elimc in - let elimt = EConstr.of_constr elimt in let i = match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause @@ -1459,7 +1455,6 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in - let ct = EConstr.of_constr ct in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in @@ -1478,7 +1473,6 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in - let t = EConstr.of_constr t in let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in let Sigma (elim, sigma, p) = @@ -1598,7 +1592,6 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = Retyping.get_type_of env sigma hyp in - let hyp_typ = EConstr.of_constr hyp_typ in let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in @@ -1662,7 +1655,6 @@ let make_projection env sigma params cstr sign elim i n c u = in let app = it_mkLambda_or_LetIn proj sign in let t = Retyping.get_type_of env sigma app in - let t = EConstr.of_constr t in Some (app, t) | None -> None in elim @@ -1673,7 +1665,6 @@ let descend_in_conjunctions avoid tac (err, info) c = let sigma = Tacmach.New.project gl in try let t = Retyping.get_type_of env sigma c in - let t = EConstr.of_constr t in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = EConstr.decompose_prod_assum sigma t in match match_with_tuple sigma ccl with @@ -1755,7 +1746,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma c)) in + let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try let n = nb_prod_modulo_zeta sigma thm_ty - nprod in @@ -1881,7 +1872,7 @@ let progress_with_clause flags innerclause clause = with Not_found -> error "Unable to unify." let apply_in_once_main flags innerclause env sigma (d,lbind) = - let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma d)) in + let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> @@ -1993,7 +1984,6 @@ let exact_check c = let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in let sigma, ct = Typing.type_of env sigma c in - let ct = EConstr.of_constr ct in let tac = Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c) in @@ -2662,9 +2652,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = | Some t -> Sigma.here t sigma | None -> let t = typ_of env sigma c in - let t = EConstr.of_constr t in let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) in let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with @@ -2717,7 +2705,7 @@ let insert_before decls lasthyp env = let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let open Context.Named.Declaration in - let t = match ty with Some t -> t | _ -> EConstr.of_constr (typ_of env sigma c) in + let t = match ty with Some t -> t | _ -> typ_of env sigma c in let decl = if dep then nlocal_def (id,c,t) else nlocal_assum (id,t) in @@ -2850,7 +2838,6 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let env = Tacmach.pf_env gl in let ids = Tacmach.pf_ids_of_hyps gl in let sigma, t = Typing.type_of env sigma c in - let t = EConstr.of_constr t in generalize_goal_gen env sigma ids i o t cl let old_generalize_dep ?(with_let=false) c gl = @@ -2923,7 +2910,6 @@ let new_generalize_gen_let lconstr = List.fold_right_i (fun i ((_,c,b),_ as o) (cl, sigma, args) -> let sigma, t = Typing.type_of env sigma c in - let t = EConstr.of_constr t in let args = if Option.is_empty b then c :: args else args in let cl, sigma = generalize_goal_gen env sigma ids i o t cl in (cl, sigma, args)) @@ -2974,7 +2960,7 @@ let specialize (c,lbind) ipat = let sigma = Typeclasses.resolve_typeclasses env sigma in sigma, nf_evar sigma c else - let clause = make_clenv_binding env sigma (c,EConstr.of_constr (Retyping.get_type_of env sigma c)) lbind in + let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -2991,7 +2977,6 @@ let specialize (c,lbind) ipat = str "."); clause.evd, term in let typ = Retyping.get_type_of env sigma term in - let typ = EConstr.of_constr typ in let tac = match EConstr.kind sigma (fst(EConstr.decompose_app sigma (snd(EConstr.decompose_lam_assum sigma c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> @@ -3699,7 +3684,6 @@ let abstract_args gl generalize_vars dep id defined f args = let argty = EConstr.of_constr argty in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in let () = sigma := sigma' in - let ty = EConstr.of_constr ty in let lenctx = List.length ctx in let liftargty = lift lenctx argty in let leq = constr_cmp !sigma Reduction.CUMUL liftargty ty in @@ -3751,7 +3735,7 @@ let abstract_args gl generalize_vars dep id defined f args = else [] in let body, c' = - if defined then Some c', EConstr.of_constr (Retyping.get_type_of ctxenv !sigma c') + if defined then Some c', Retyping.get_type_of ctxenv !sigma c' else None, c' in let typ = Tacmach.pf_get_hyp_typ gl id in @@ -4339,7 +4323,6 @@ let clear_unselected_context id inhyps cls = let use_bindings env sigma elim must_be_closed (c,lbind) typ = let sigma = Sigma.to_evar_map sigma in - let typ = EConstr.of_constr typ in let typ = if elim == None then (* w/o an scheme, the term has to be applied at least until @@ -4389,7 +4372,6 @@ let check_enough_applied env sigma elim = let t,_ = decompose_app sigma (whd_all env sigma u) in isInd sigma t | Some elimc -> let elimt = Retyping.get_type_of env sigma (fst elimc) in - let elimt = EConstr.of_constr elimt in let scheme = compute_elim_sig sigma ~elimc elimt in match scheme.indref with | None -> @@ -4435,7 +4417,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim let b = not with_evars && with_eq != None in let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in - let t = EConstr.of_constr t in let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in Sigma (ans, sigma, p +> q) end }; @@ -4487,7 +4468,7 @@ let induction_gen clear_flag isrec with_evars elim && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in - let enough_applied = check_enough_applied env sigma elim (EConstr.of_constr t) in + let enough_applied = check_enough_applied env sigma elim t in if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and with maximal abstraction over the variable. @@ -4504,6 +4485,7 @@ let induction_gen clear_flag isrec with_evars elim declaring the induction argument as a new local variable *) let id = (* Type not the right one if partially applied but anyway for internal use*) + let t = EConstr.Unsafe.to_constr t in let x = id_of_name_using_hdchar (Global.env()) t Anonymous in new_fresh_id [] x gl in let info_arg = (is_arg_pure_hyp, not enough_applied) in diff --git a/toplevel/command.ml b/toplevel/command.ml index 820c1b885..1fc89b8b0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -206,7 +206,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> Retyping.get_type_of env evd (EConstr.of_constr c) + | None -> EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = @@ -459,7 +459,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))) + (nf_evar evd (EConstr.Unsafe.to_constr (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) @@ -1106,6 +1106,7 @@ let interp_recursive isfix fixl notations = (fun env' id t -> if Flags.is_program_mode () then let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref (EConstr.of_constr t) in + let sort = EConstr.Unsafe.to_constr sort in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 9ed34d713..21bc895a8 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -404,6 +404,7 @@ let do_mutual_induction_scheme lnamedepindsort = let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in + let decltype = EConstr.to_constr sigma decltype in let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref |