diff options
36 files changed, 310 insertions, 257 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 62627a416..fc193b94a 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -278,17 +278,20 @@ let make_pure_subst evi args = *) let csubst_subst (k, s) c = + (** Safe because this is a substitution *) + let c = EConstr.Unsafe.to_constr c in let rec subst n c = match Constr.kind c with | Rel m -> if m <= n then c - else if m - n <= k then Int.Map.find (k - m + n) s + else if m - n <= k then EConstr.Unsafe.to_constr (Int.Map.find (k - m + n) s) else mkRel (m - k) | _ -> Constr.map_with_binders succ subst n c in - if k = 0 then c else subst 0 c + let c = if k = 0 then c else subst 0 c in + EConstr.of_constr c let subst2 subst vsubst c = - csubst_subst subst (replace_vars vsubst c) + csubst_subst subst (EConstr.Vars.replace_vars vsubst c) let next_ident_away id avoid = let avoid id = Id.Set.mem id avoid in @@ -299,24 +302,29 @@ let next_name_away na avoid = let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in next_ident_away_from id avoid -type csubst = int * Constr.t Int.Map.t +type csubst = int * EConstr.t Int.Map.t let empty_csubst = (0, Int.Map.empty) type ext_named_context = - csubst * (Id.t * Constr.constr) list * + csubst * (Id.t * EConstr.constr) list * Id.Set.t * Context.Named.t let push_var id (n, s) = - let s = Int.Map.add n (mkVar id) s in + let s = Int.Map.add n (EConstr.mkVar id) s in (succ n, s) let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = + let open EConstr in + let open Vars in + let map_decl f d = + NamedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (f (EConstr.of_constr c))) d + in let replace_var_named_declaration id0 id decl = let id' = NamedDecl.get_id decl in let id' = if Id.equal id0 id' then id else id' in let vsubst = [id0 , mkVar id] in - decl |> NamedDecl.set_id id' |> NamedDecl.map_constr (replace_vars vsubst) + decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst) in let extract_if_neq id = function | Anonymous -> None @@ -344,7 +352,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = context. Unless [id] is a section variable. *) let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in let vsubst = (id0,mkVar id)::vsubst in - let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> NamedDecl.map_constr (subst2 subst vsubst) in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (subst2 subst vsubst) in let nc = List.map (replace_var_named_declaration id0 id) nc in (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc) | _ -> @@ -352,7 +360,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) = incorrect. We revert to a less robust behaviour where the new binder has name [id]. Which amounts to the same behaviour than when [id=id0]. *) - let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> NamedDecl.map_constr (subst2 subst vsubst) in + let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (subst2 subst vsubst) in (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc) let push_rel_context_to_named_context env typ = @@ -391,6 +399,7 @@ let new_pure_evar_full evd evi = Sigma.Unsafe.of_pair (evk, evd) let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = + let typ = EConstr.Unsafe.to_constr typ in let evd = Sigma.to_evar_map evd in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in @@ -420,7 +429,8 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin (* Converting the env into the sign of the evar to define *) let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in - let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in + let map c = EConstr.Unsafe.to_constr (subst2 subst vsubst (EConstr.of_constr c)) in + let candidates = Option.map (fun l -> List.map map l) candidates in let instance = match filter with | None -> instance @@ -434,7 +444,7 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t let new_type_evar env evd ?src ?filter ?naming ?principal rigid = let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in - let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in + let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in Sigma ((e, s), evd', p +> q) let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = @@ -753,5 +763,5 @@ let eq_constr_univs_test sigma1 sigma2 t u = in match ans with None -> false | Some _ -> true -type type_constraint = types option -type val_constraint = constr option +type type_constraint = EConstr.types option +type val_constraint = EConstr.constr option diff --git a/engine/evarutil.mli b/engine/evarutil.mli index d6e2d4534..dcb9bf247 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -24,13 +24,13 @@ val new_evar : env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (constr, 'r) Sigma.sigma + ?principal:bool -> EConstr.types -> (constr, 'r) Sigma.sigma val new_pure_evar : named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (evar, 'r) Sigma.sigma + ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma @@ -39,7 +39,7 @@ val e_new_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr + ?principal:bool -> EConstr.types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) @@ -70,7 +70,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> 'r Sigma.t -> types -> + named_context_val -> 'r Sigma.t -> EConstr.types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> @@ -208,17 +208,17 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty type csubst val empty_csubst : csubst -val csubst_subst : csubst -> Constr.t -> Constr.t +val csubst_subst : csubst -> EConstr.t -> EConstr.t type ext_named_context = - csubst * (Id.t * Constr.constr) list * + csubst * (Id.t * EConstr.constr) list * Id.Set.t * Context.Named.t val push_rel_decl_to_named_context : Context.Rel.Declaration.t -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * csubst * (identifier*constr) list +val push_rel_context_to_named_context : Environ.env -> EConstr.types -> + named_context_val * EConstr.types * constr list * csubst * (identifier*EConstr.constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list @@ -235,5 +235,5 @@ val meta_counter_summary_name : string (** Deprecater *) -type type_constraint = types option -type val_constraint = constr option +type type_constraint = EConstr.types option +type val_constraint = EConstr.constr option diff --git a/engine/proofview.ml b/engine/proofview.ml index 21227ed19..b0f6d463b 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -71,7 +71,7 @@ let dependent_init = | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in + let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in let sigma = Sigma.to_evar_map sigma in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 235e6e24f..8d4d87f2a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1937,7 +1937,7 @@ let extract_ids env = let scope_of_type_kind = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope typ + | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ) | WithoutTypeConstraint -> None let empty_ltac_sign = { @@ -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 typ) env sigma ~impls c + interp_gen (OfType (EConstr.of_constr 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 typ) c + interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls IsType c @@ -2016,7 +2016,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType typ) c + interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref IsType ~impls c @@ -2102,7 +2102,7 @@ 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 t) b in + let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b 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/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index 5d3b2b886..99023fdbb 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -85,7 +85,7 @@ let let_evar name typ = Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) | Names.Name id -> id in - let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in + let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) (EConstr.of_constr typ) in let tac = (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) in diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 53b726432..f8db0b4fc 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 (pf_concl gl)) ist (pf_env gl) (project gl) c + interp_constr_gen (Pretyping.OfType (EConstr.of_constr (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 e1b468197..981ff549d 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -351,7 +351,7 @@ let refine_tac ist simple c = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = constr_flags in - let expected_type = Pretyping.OfType concl in + let expected_type = Pretyping.OfType (EConstr.of_constr concl) in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in let refine = Refine.refine ~unsafe:true update in diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 58153c453..ccd45756a 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -95,7 +95,7 @@ let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = let s = Typeclasses.set_resolvable Evd.Store.empty false in let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in + let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd (EConstr.of_constr t) in let evd' = Sigma.to_evar_map evd' in let ev, _ = destEvar t in (evd', Evar.Set.add ev cstrs), t @@ -1549,8 +1549,8 @@ let assert_replacing id newt tac = in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> - let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in - let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in + let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma (EConstr.of_constr concl) in + let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in let map d = let n = NamedDecl.get_id d in if Id.equal n id then ev' else mkVar n @@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let make = { run = begin fun sigma -> - let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in + let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in Sigma (mkApp (p, [| ev |]), sigma, q) end } in Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls @@ -1926,7 +1926,7 @@ let build_morphism_signature env sigma m = let evd = solve_constraints env !evd in let evd = Evd.nf_constraints evd in let m = Evarutil.nf_evars_universes evd morph in - Pretyping.check_evars env Evd.empty evd m; + Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m let default_morphism sign m = diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 65d273faf..ddf013735 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -173,7 +173,7 @@ let get_eq_typ info env = typ let interp_constr_in_type typ env sigma c = - fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*) + fst (understand env sigma (fst c) ~expected_type:(OfType (EConstr.of_constr typ)))(*FIXME*) let interp_statement interp_it env sigma st = {st_label=st.st_label; diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e587fd52c..5e16d2da0 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1330,7 +1330,7 @@ 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 concl) (frob rawc) + Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType (EConstr.of_constr concl)) (frob rawc) let my_refine c gls = let oc = { run = begin fun sigma -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1a181202c..92bd1e389 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -301,7 +301,7 @@ let inductive_template evdref env tmloc ind = | LocalAssum (na,ty) -> let ty = EConstr.of_constr ty in let ty' = substl subst ty in - let e = EConstr.of_constr (e_new_evar env evdref ~src:(hole_source n) (EConstr.Unsafe.to_constr ty')) in + let e = EConstr.of_constr (e_new_evar env evdref ~src:(hole_source n) ty') in (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> let b = EConstr.of_constr b in @@ -1665,6 +1665,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = (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 let ev' = EConstr.of_constr ev' in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with @@ -1700,7 +1701,6 @@ let abstract_tycon loc env evdref subst tycon extenv t = let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in let candidates = List.map EConstr.Unsafe.to_constr candidates in - let ty = EConstr.Unsafe.to_constr ty in let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in let ev = EConstr.of_constr ev in lift k ev @@ -2469,7 +2469,6 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in let tycon = valcon_of_tycon tycon in - let tycon = Option.map EConstr.of_constr tycon in let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in let env = push_rel_context tomatchs_lets env in let len = List.length eqns in @@ -2583,7 +2582,6 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e with the type of arguments to match; if none is provided, we build alternative possible predicates *) let arsign = extract_arity_signature env tomatchs tomatchl in - let tycon = Option.map EConstr.of_constr tycon in let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index cc121a96d..b9f14aa43 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -93,7 +93,7 @@ open Program let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in - EConstr.of_constr (Evarutil.e_new_evar env evdref ~src (EConstr.Unsafe.to_constr c)) + EConstr.of_constr (Evarutil.e_new_evar env evdref ~src c) let app_opt env evdref f t = EConstr.of_constr (whd_betaiota !evdref (app_opt f t)) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cdcb993b5..683b33b89 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -338,7 +338,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) - env evd (EConstr.Unsafe.to_constr term1) (EConstr.Unsafe.to_constr term2) + env evd term1 term2 in if b then Success evd else UnifFailure (evd, ConversionFailed (env,term1,term2)) @@ -891,7 +891,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) else let dloc = (Loc.ghost,Evar_kinds.InternalHole) in let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (EConstr.Unsafe.to_constr (Vars.substl ks b)) in + let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (Vars.substl ks b) in let i' = Sigma.to_evar_map i' in (i', EConstr.of_constr ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs @@ -1075,7 +1075,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let evty = set_holes evdref cty subst in let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (ev, evd, _) = new_evar_instance sign evd (EConstr.Unsafe.to_constr evty) ~filter instance in + let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in let evd = Sigma.to_evar_map evd in evdref := evd; evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref; diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f372dbf06..ff40a6938 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -39,9 +39,9 @@ let env_nf_betaiotaevar sigma env = (* Operations on value/type constraints *) (****************************************) -type type_constraint = types option +type type_constraint = EConstr.types option -type val_constraint = constr option +type val_constraint = EConstr.constr option (* Old comment... * Basically, we have the following kind of constraints (in increasing @@ -61,13 +61,13 @@ type val_constraint = constr option let empty_tycon = None (* Builds a type constraint *) -let mk_tycon ty = Some (EConstr.Unsafe.to_constr ty) +let mk_tycon ty = Some ty (* Constrains the value of a type *) let empty_valcon = None (* Builds a value constraint *) -let mk_valcon c = Some (EConstr.Unsafe.to_constr c) +let mk_valcon c = Some c let idx = Namegen.default_dependent_ident @@ -80,7 +80,8 @@ let define_pure_evar_as_product evd evk = let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in - let s = destSort evd (EConstr.of_constr concl) in + let concl = EConstr.of_constr concl in + let s = destSort evd concl in let evd1,(dom,u1) = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in @@ -146,7 +147,7 @@ let define_pure_evar_as_lambda env evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in - let evd2,body = new_evar_unsafe newenv evd1 ~src (EConstr.Unsafe.to_constr (Vars.subst1 (mkVar id) rng)) ~filter in + let evd2,body = new_evar_unsafe newenv evd1 ~src (Vars.subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, EConstr.of_constr dom, Vars.subst_var id (EConstr.of_constr body)) in Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam @@ -203,12 +204,12 @@ let split_tycon loc env evd tycon = match tycon with | None -> evd,(Anonymous,None,None) | Some c -> - let evd', (n, dom, rng) = real_split evd (EConstr.of_constr c) in + let evd', (n, dom, rng) = real_split evd c in evd', (n, mk_tycon dom, mk_tycon rng) let valcon_of_tycon x = x -let lift_tycon n = Option.map (lift n) +let lift_tycon n = Option.map (EConstr.Vars.lift n) let pr_tycon env = function None -> str "None" - | Some t -> Termops.print_constr_env env t + | Some t -> Termops.print_constr_env env (EConstr.Unsafe.to_constr t) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index f7bf4636b..9c03a6e3f 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -8,6 +8,7 @@ open Names open Term +open EConstr open Evd open Environ @@ -18,16 +19,16 @@ type type_constraint = types option type val_constraint = constr option val empty_tycon : type_constraint -val mk_tycon : EConstr.constr -> type_constraint +val mk_tycon : constr -> type_constraint val empty_valcon : val_constraint -val mk_valcon : EConstr.constr -> val_constraint +val mk_valcon : constr -> val_constraint (** Instantiate an evar by as many lambda's as needed so that its arguments are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into [?y[vars1:=args1,vars:=args]] with [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *) -val evar_absorb_arguments : env -> evar_map -> EConstr.existential -> EConstr.constr list -> - evar_map * EConstr.existential +val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> + evar_map * existential val split_tycon : Loc.t -> env -> evar_map -> type_constraint -> @@ -36,9 +37,9 @@ val split_tycon : val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint -val define_evar_as_product : evar_map -> EConstr.existential -> evar_map * EConstr.types -val define_evar_as_lambda : env -> evar_map -> EConstr.existential -> evar_map * EConstr.types -val define_evar_as_sort : env -> evar_map -> EConstr.existential -> evar_map * sorts +val define_evar_as_product : evar_map -> existential -> evar_map * types +val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts (** {6 debug pretty-printer:} *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 8a22aed2f..3bcea4cee 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -606,7 +606,7 @@ 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 open EConstr in let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src (List.map EConstr.Unsafe.to_constr inst_in_env) in + let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src (List.map EConstr.Unsafe.to_constr 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 evar_in_env = EConstr.of_constr evar_in_env in @@ -682,6 +682,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = 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 (List.map EConstr.Unsafe.to_constr inst2_in_sign) in let evd = Sigma.to_evar_map evd in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index c8bcae0c8..ff3424c44 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -409,7 +409,5 @@ let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t let native_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = - let t1 = EConstr.Unsafe.to_constr t1 in - let t2 = EConstr.Unsafe.to_constr t2 in Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma) ~catch_incon:true ~pb env sigma t1 t2 diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 18731f1e9..cac31a1c5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -27,8 +27,9 @@ open Util open Names open Evd open Term -open Vars open Termops +open EConstr +open Vars open Reductionops open Environ open Type_errors @@ -59,7 +60,7 @@ type ltac_var_map = { ltac_genargs : unbound_ltac_var_map; } type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * constr +type pure_open_constr = evar_map * Constr.constr (************************************************************************) (* This concerns Cases *) @@ -68,6 +69,16 @@ open Inductiveops (************************************************************************) +let local_assum (na, t) = + let open Context.Rel.Declaration in + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let open Context.Rel.Declaration in + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + module ExtraEnv = struct @@ -104,7 +115,7 @@ let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in + let inst_vars = List.map (get_id %> Constr.mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in let (subst, vsubst, _, nc) = Lazy.force env.extra in let typ' = subst2 subst vsubst typ in @@ -116,7 +127,7 @@ let e_new_evar env evdref ?src ?naming typ = e let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt end @@ -127,6 +138,13 @@ open ExtraEnv exception Found of int array +let nf_fix sigma (nas, cs, ts) = + let inj c = EConstr.to_constr sigma c in + (nas, Array.map inj cs, Array.map inj ts) + +let nf_evar sigma c = + EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) + let search_guard loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) @@ -282,7 +300,7 @@ let apply_inference_hook hook evdref pending = then try let sigma, c = hook sigma evk in - Evd.define evk c sigma + Evd.define evk (EConstr.Unsafe.to_constr c) sigma with Exit -> sigma else @@ -313,17 +331,15 @@ let check_extra_evars_are_solved env current_sigma pending = let check_evars env initial_sigma sigma c = let rec proc_rec c = - match kind_of_term c with - | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with - | Some c -> proc_rec c - | None -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None) - | _ -> Constr.iter proc_rec c + match EConstr.kind sigma c with + | Evar (evk, _) -> + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk sigma in + begin match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None + end + | _ -> EConstr.iter sigma proc_rec c in proc_rec c let check_evars_are_solved env current_sigma frozen pending = @@ -359,7 +375,7 @@ let allow_anonymous_refs = ref false let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j (EConstr.of_constr t) + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -409,26 +425,29 @@ 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 Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma (EConstr.of_constr c) + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> user_err - (str "Cannot reinterpret " ++ quote (print_constr c) ++ + (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++ str " in the current environment.") +let j_val j = EConstr.of_constr (j_val j) + let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in - { uj_val = mkRel n; uj_type = lift n typ } + let typ = EConstr.of_constr typ in + { uj_val = EConstr.Unsafe.to_constr (mkRel n); uj_type = EConstr.Unsafe.to_constr (lift n typ) } with Not_found -> let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in let subst = List.map (invert_ltac_bound_name lvar env id) ids in - let c = substl subst c in - { uj_val = c; uj_type = protected_get_type_of env sigma c } + let c = substl subst (EConstr.of_constr c) in + { uj_val = EConstr.Unsafe.to_constr c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in let lvar = { @@ -453,14 +472,11 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } + { uj_val = Constr.mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found ~loc id -let evar_kind_of_term sigma c = - kind_of_term (whd_evar sigma c) - (*************************************************************************) (* Main pretyping function *) @@ -492,13 +508,17 @@ let pretype_global loc rigid env evd gr us = str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in - Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr + let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in + (sigma, EConstr.of_constr c) + +let make_judge c t = + make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) + (try make_judge (mkVar id) (EConstr.of_constr (NamedDecl.get_type (lookup_named id env))) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -507,13 +527,14 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in + let ty = Typing.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 = let evd, s = interp_universe ~loc evd s in let judge = - { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } + { uj_val = Constr.mkSort (Type s); uj_type = Constr.mkSort (Type (Univ.super s)) } in evd, judge @@ -563,32 +584,32 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref (EConstr.of_constr c)) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> ty + | Some ty -> EConstr.Unsafe.to_constr ty | None -> new_type_evar env evdref loc in let k = Evar_kinds.MatchingVar (someta,n) in - { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) (EConstr.of_constr ty); uj_type = ty } | GHole (loc, k, naming, None) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> ty + | Some ty -> EConstr.Unsafe.to_constr ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming (EConstr.of_constr ty); uj_type = ty } | GHole (loc, k, _naming, Some arg) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> ty + | Some ty -> EConstr.Unsafe.to_constr ty | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in @@ -616,8 +637,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (fun e ar -> pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) ctxtv lar in - let lara = Array.map (fun a -> a.utj_val) larj in - let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in + let lara = Array.map (fun a -> EConstr.of_constr a.utj_val) larj in + let ftys = Array.map2 (fun e a -> EConstr.it_mkProd_or_LetIn a e) ctxtv lara in let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in let _ = @@ -626,7 +647,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env.ExtraEnv.env evdref (EConstr.of_constr ftys.(fixi)) (EConstr.of_constr t) + in e_conv env.ExtraEnv.env evdref ftys.(fixi) t | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -637,16 +658,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) let (ctxt,ty) = - decompose_prod_n_assum (Context.Rel.length ctxt) + decompose_prod_n_assum !evdref (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon (EConstr.of_constr ty)) nenv evdref lvar def in - { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) + let j = pretype (mk_tycon ty) nenv evdref lvar def in + { uj_val = Termops.it_mkLambda_or_LetIn j.uj_val ctxt; + uj_type = Termops.it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj; - let ftys = Array.map (nf_evar !evdref) ftys in - let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in + Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; + let nf c = nf_evar !evdref c in + let ftys = Array.map nf ftys in (** FIXME *) + let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in let fixj = match fixkind with | GFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -665,12 +687,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env.ExtraEnv.env possible_indexes fixdecls + loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> - let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env.ExtraEnv.env cofix + let fixdecls = (names,ftys,fdefs) in + let cofix = (i, fixdecls) in + (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls) with reraise -> let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in @@ -691,24 +714,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Bidirectional typechecking hint: parameters of a constructor are completely determined by a typing constraint *) - if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then + if Flags.is_program_mode () && length > 0 && isConstruct !evdref (EConstr.of_constr fj.uj_val) then match tycon with | None -> [] | Some ty -> - let ((ind, i), u) = destConstruct fj.uj_val in + let ((ind, i), u) = destConstruct !evdref (EConstr.of_constr fj.uj_val) in let npars = inductive_nparams ind in if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr ty) in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in - if eq_ind ind ind' then pars + if eq_ind ind ind' then List.map EConstr.of_constr pars else (* Let the usual code throw an error *) [] with Not_found -> [] else [] in let app_f = - match kind_of_term fj.uj_val with + match EConstr.kind !evdref (EConstr.of_constr fj.uj_val) with | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in let pb = Environ.lookup_projection p env.ExtraEnv.env in @@ -724,7 +747,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in let resty = whd_all env.ExtraEnv.env !evdref (EConstr.of_constr resj.uj_type) in - match kind_of_term resty with + let resty = EConstr.of_constr resty in + match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> let tycon = Some c1 in let hj = pretype tycon env evdref lvar c in @@ -732,12 +756,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env.ExtraEnv.env evdref (EConstr.of_constr (j_val hj)) (EConstr.of_constr arg) then + if e_conv env.ExtraEnv.env evdref (j_val hj) arg then args, nf_evar !evdref (j_val hj) else [], j_val hj in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in + let j = { uj_val = EConstr.Unsafe.to_constr value; uj_type = EConstr.Unsafe.to_constr typ } in apply_rec env (n+1) j candargs rest | _ -> @@ -748,16 +772,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let resj = apply_rec env 1 fj candargs args in let resj = - match evar_kind_of_term !evdref resj.uj_val with + match EConstr.kind !evdref (EConstr.of_constr resj.uj_val) with | App (f,args) -> - let f = whd_evar !evdref f in - if is_template_polymorphic env.ExtraEnv.env !evdref (EConstr.of_constr f) then + if is_template_polymorphic env.ExtraEnv.env !evdref f then (* Special case for inductive type applications that must be refreshed right away. *) - let sigma = !evdref in - let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref (EConstr.of_constr c) in - let t = Retyping.get_type_of env.ExtraEnv.env !evdref (EConstr.of_constr c) in + 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 @@ -770,8 +794,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd (EConstr.of_constr ty) in - evd, Some (EConstr.Unsafe.to_constr ty')) + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in + evd, Some ty') evdref tycon in let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in @@ -794,7 +818,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in - { j with utj_val = lift 1 j.utj_val } + { j with utj_val = EConstr.Unsafe.to_constr (lift 1 (EConstr.of_constr j.utj_val)) } | Name _ -> let var = LocalAssum (name, j.utj_val) in let env' = push_rel var env in @@ -825,11 +849,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre the substitution must also be applied on variables before they are looked up in the rel context. *) let var = LocalDef (name, j.uj_val, t) in + let t = EConstr.of_constr t in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; - uj_type = subst1 j.uj_val j'.uj_type } + { uj_val = EConstr.Unsafe.to_constr (mkLetIn (name, EConstr.of_constr j.uj_val, t, EConstr.of_constr j'.uj_val)) ; + uj_type = EConstr.Unsafe.to_constr (subst1 (EConstr.of_constr j.uj_val) (EConstr.of_constr j'.uj_type)) } | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in @@ -839,6 +864,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in + let realargs = List.map EConstr.of_constr realargs in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err ~loc (str "Destructing let is only for inductive types" ++ @@ -855,8 +881,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let rec aux n k names l = match names, l with | na :: names, (LocalAssum (_,t) :: l) -> + let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) + local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, EConstr.of_constr cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -870,7 +897,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) + mkCase (ci, p, EConstr.of_constr cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in @@ -887,28 +914,28 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref pj.utj_val in + let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = - (Array.to_list cs.cs_concl_realargs) - @[build_dependent_constructor cs] in + (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) + @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env.ExtraEnv.env !evdref (EConstr.of_constr lp) (List.map EConstr.of_constr inst) in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); - obj ind p cj.uj_val fj.uj_val + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; + obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } + { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr (substl (realargs@[EConstr.of_constr cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f evdref lvar d in - let ccl = nf_evar !evdref fj.uj_type in + let ccl = nf_evar !evdref (EConstr.of_constr fj.uj_type) in let ccl = - if noccur_between 1 cs.cs_nargs ccl then + if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else error_cant_find_case_type ~loc env.ExtraEnv.env !evdref @@ -917,9 +944,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); - obj ind p cj.uj_val fj.uj_val - in { uj_val = v; uj_type = ccl }) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; + obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) + in { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in @@ -946,16 +973,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref pj.utj_val in + let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (beta_applist !evdref (EConstr.of_constr pred,[EConstr.of_constr cj.uj_val])) in + let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[EConstr.of_constr cj.uj_val]))) in pred, typ | None -> let p = match tycon with | Some ty -> ty | None -> let env = ltac_interp_name_env k0 lvar env in - new_type_evar env evdref loc + EConstr.of_constr (new_type_evar env evdref loc) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -963,7 +990,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let f cs b = let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) - let pi = beta_applist !evdref (EConstr.of_constr pi, [EConstr.of_constr (build_dependent_constructor cs)]) in + let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args @@ -974,17 +1001,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in + it_mkLambda_or_LetIn (EConstr.of_constr bj.uj_val) cs.cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred); - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) pred; + mkCase (ci, pred, EConstr.of_constr cj.uj_val, [|b1;b2|]) in - let cj = { uj_val = v; uj_type = p } in + let cj = { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr p } in inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> @@ -1004,53 +1031,56 @@ 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 (EConstr.of_constr 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 -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in - if not (occur_existential !evdref (EConstr.of_constr cty) || occur_existential !evdref (EConstr.of_constr tval)) then + let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in + if not (occur_existential !evdref cty || occur_existential !evdref tval) then let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) + error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ~loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in + let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref (EConstr.of_constr cty) (EConstr.of_constr tval) in + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) + error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> - pretype (mk_tycon (EConstr.of_constr tval)) env evdref lvar c, tval + pretype (mk_tycon tval) env evdref lvar c, tval in - let v = mkCast (cj.uj_val, k, tval) in - { uj_val = v; uj_type = tval } + let v = mkCast (EConstr.of_constr cj.uj_val, k, tval) in + { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = let id = NamedDecl.get_id decl in - let t = replace_vars subst (NamedDecl.get_type decl) in + let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in let c, update = try let c = List.assoc id update in - let c = pretype k0 resolve_tc (mk_tycon (EConstr.of_constr t)) env evdref lvar c in - c.uj_val, List.remove_assoc id update + let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in + EConstr.of_constr c.uj_val, List.remove_assoc id update with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref (EConstr.of_constr t) (EConstr.of_constr t') then mkRel n, update else raise Not_found + let t' = EConstr.of_constr t' in + if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in - if is_conv env.ExtraEnv.env !evdref (EConstr.of_constr t) (EConstr.of_constr t') then mkVar id, update else raise Not_found + let t' = EConstr.of_constr t' in + if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err ~loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1063,18 +1093,23 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> + let rec is_Type c = match EConstr.kind !evdref c with + | Sort (Type _) -> true + | Cast (c, _, _) -> is_Type c + | _ -> false + in (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env.ExtraEnv.env sigma (EConstr.of_constr v) in + let t = Retyping.get_type_of env.ExtraEnv.env sigma v in match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with | Sort s -> s - | Evar ev when is_Type (existential_type sigma (fst ev, Array.map EConstr.Unsafe.to_constr (snd ev))) -> + | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in - { utj_val = v; + { utj_val = EConstr.Unsafe.to_constr v; utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env in @@ -1088,10 +1123,10 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref (EConstr.of_constr v) (EConstr.of_constr tj.utj_val) then tj + if e_cumul env.ExtraEnv.env evdref v (EConstr.of_constr tj.utj_val) then tj else error_unexpected_type - ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val (EConstr.Unsafe.to_constr v) let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env in @@ -1101,11 +1136,11 @@ let ise_pretype_gen flags env sigma lvar kind c = | WithoutTypeConstraint -> (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon (EConstr.of_constr exptyp)) env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,EConstr.of_constr c') let default_inference_flags fail = { use_typeclasses = true; @@ -1131,17 +1166,17 @@ let empty_lvar : ltac_var_map = { ltac_genargs = Id.Map.empty; } -let on_judgment f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast (f c) in - {uj_val = c; uj_type = t} +let on_judgment sigma f j = + let c = mkCast(EConstr.of_constr j.uj_val,DEFAULTcast, EConstr.of_constr j.uj_type) in + let (c,_,t) = destCast sigma (f c) in + {uj_val = EConstr.Unsafe.to_constr c; uj_type = EConstr.Unsafe.to_constr t} let understand_judgment env sigma c = let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment (fun c -> + let j = on_judgment sigma (fun c -> let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref @@ -1150,14 +1185,14 @@ let understand_judgment_tcc env evdref c = let env = make_env env in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment (fun c -> + on_judgment !evdref (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in evdref := evd; c) j let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in - f c, Evd.evar_universe_context evd + f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) @@ -1168,15 +1203,17 @@ let understand ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = - ise_pretype_gen flags env sigma empty_lvar expected_type c + let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in + (sigma, EConstr.Unsafe.to_constr 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; - c + EConstr.Unsafe.to_constr c let understand_ltac flags env sigma lvar kind c = - ise_pretype_gen 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) let constr_flags = { use_typeclasses = true; diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e09648ec3..603b9f9ea 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -25,7 +25,7 @@ open Misctypes val search_guard : Loc.t -> env -> int list list -> rec_declaration -> int array -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = OfType of EConstr.types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t @@ -47,7 +47,7 @@ val empty_lvar : ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -type inference_hook = env -> evar_map -> evar -> evar_map * constr +type inference_hook = env -> evar_map -> evar -> evar_map * EConstr.constr type inference_flags = { use_typeclasses : bool; @@ -139,7 +139,7 @@ val check_evars_are_solved : (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> constr -> unit +val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit (**/**) (** Internal of Pretyping... *) @@ -153,7 +153,7 @@ val pretype_type : val ise_pretype_gen : inference_flags -> env -> evar_map -> - ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * EConstr.constr (**/**) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 69d47e8e6..0b97cd253 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1317,6 +1317,8 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in try let fold cstr sigma = try Some (Evd.add_universe_constraints sigma cstr) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 911dab0b6..5e6a40786 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -264,12 +264,12 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> ECo otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> - env -> evar_map -> constr -> constr -> evar_map * bool + env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool (** Conversion with inference of universe constraints *) -val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> +val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool) -> unit -val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> +val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool @@ -278,7 +278,7 @@ conversion function. Used to pretype vm and native casts. *) val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> (constr, evar_map) Reduction.generic_conversion_function) -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> - evar_map -> constr -> constr -> evar_map * bool + evar_map -> EConstr.constr -> EConstr.constr -> evar_map * bool (** {6 Special-Purpose Reduction Functions } *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b729f3b9b..5b8eaa50b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -413,7 +413,7 @@ let substl_with_function subst sigma constr = match v.(i-k-1) with | (fx, Some (min, ref)) -> let sigma = Sigma.Unsafe.of_evar_map !evd in - let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma (EConstr.of_constr dummy) in let sigma = Sigma.to_evar_map sigma in evd := sigma; minargs := Evar.Map.add evk min !minargs; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b568dd044..70aa0be6b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -167,6 +167,7 @@ let pose_all_metas_as_evars env evd t = let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in let src = Evd.evar_source_of_meta mv !evdref in + let ty = EConstr.of_constr ty in let ev = Evarutil.e_new_evar env evdref ~src ty in evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; ev) @@ -608,7 +609,7 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = | None -> sigma | Some n -> if is_ground_term sigma (EConstr.of_constr m) && is_ground_term sigma (EConstr.of_constr n) then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in + let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma (EConstr.of_constr m) (EConstr.of_constr n) in if b then sigma else error_cannot_unify env sigma (m,n) else sigma @@ -961,10 +962,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (* Renounce, maybe metas/evars prevents typing *) sigma else sigma in + let m1 = EConstr.of_constr m1 and n1 = EConstr.of_constr n1 in let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in if b then Some (sigma, metasubst, evarsubst) else - if is_ground_term sigma (EConstr.of_constr m1) && is_ground_term sigma (EConstr.of_constr n1) then + if is_ground_term sigma m1 && is_ground_term sigma n1 then error_cannot_unify curenv sigma (cM,cN) else None in @@ -1071,7 +1073,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb None else let sigma, b = match flags.modulo_conv_on_closed_terms with - | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n + | Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma (EConstr.of_constr m) (EConstr.of_constr n) | _ -> constr_cmp cv_pb sigma flags m n in if b then Some sigma else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with @@ -1210,7 +1212,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = else match kind_of_term (whd_all env (Sigma.to_evar_map evd) (EConstr.of_constr cty)) with | Prod (_,c1,c2) -> - let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in + let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) (EConstr.of_constr c1) in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in @@ -1570,7 +1572,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1,x), Some (_,c2,_) -> - let (evd,b) = infer_conv ~pb:CONV env evd (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in + let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in if b then Some (evd, c1, x) else raise (NotUnifiable None) | Some _, None -> c1 | None, Some _ -> c2 @@ -1883,7 +1885,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in - let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in + let evd', b = infer_conv ~pb:CUMUL env evd' (EConstr.of_constr predtyp) (EConstr.of_constr typp) in if not b then error_wrong_abstraction_type env evd' (Evd.meta_name evd p) pred typp predtyp; @@ -1900,7 +1902,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let secondOrderDependentAbstraction env evd flags typ (p, oplist) = let typp = Typing.meta_type evd p in - let evd, pred = abstract_list_all_with_dependencies env evd typp typ (List.map EConstr.of_constr oplist) in + let evd, pred = abstract_list_all_with_dependencies env evd (EConstr.of_constr typp) typ (List.map EConstr.of_constr oplist) in w_merge env false flags.merge_unify_flags (evd,[p,pred,(Conv,TypeProcessed)],[]) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0515e4198..68aeaef5e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -337,7 +337,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = Sigma.Unsafe.of_evar_map clenv.evd in - let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in @@ -610,7 +610,7 @@ let make_evar_clause env sigma ?len t = | Prod (na, t1, t2) -> let store = Typeclasses.set_resolvable Evd.Store.empty false in let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in let sigma = Sigma.to_evar_map sigma in let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in let hole = { diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index af5fa921f..fd6528a1e 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -51,7 +51,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags - env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc + env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err ~loc diff --git a/proofs/logic.ml b/proofs/logic.ml index 93b31ced1..093d949d5 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -314,7 +314,7 @@ let check_meta_variables c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma ty conclty in + let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm else raise (RefinerError (BadType (arg,ty,conclty))) else sigma diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 67e216745..af910810b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -236,6 +236,6 @@ let solve_by_implicit_tactic env sigma evk = let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in let sigma = Evd.set_universe_context sigma ctx in - sigma, ans + sigma, EConstr.of_constr ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7458109fa..807a554df 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ff7dbfa91..bc1d0ed6b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1458,7 +1458,7 @@ let _ = let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in let (gl,t,sigma) = - Goal.V82.mk_goal sigma nc gl Store.empty in + Goal.V82.mk_goal sigma nc (EConstr.Unsafe.to_constr gl) Store.empty in let gls = { it = gl ; sigma = sigma; } in let hints = searchtable_map typeclasses_db in let st = Hint_db.transparent_state hints in @@ -1481,7 +1481,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = let _ = Hook.set Typeclasses.solve_one_instance_hook - (fun x y z w -> resolve_one_typeclass x ~sigma:y (EConstr.Unsafe.to_constr z) w) + (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) (** Take the head of the arity of a constr. Used in the partial application tactic. *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 9679ac402..be175937b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1176,7 +1176,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with | (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in - let ev = Evarutil.e_new_evar env evdref a in + let ev = Evarutil.e_new_evar env evdref (EConstr.of_constr a) in let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[EConstr.of_constr ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in match diff --git a/tactics/hints.ml b/tactics/hints.ml index b2aa02191..e8225df2d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1213,7 +1213,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = subst := (evar,mkVar id)::!subst; mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in let c' = iter c in - if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c'; + if check then Pretyping.check_evars (Global.env()) Evd.empty sigma (EConstr.of_constr c'); let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a6bc805bd..3bb285aa8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -176,7 +176,7 @@ let unsafe_intro env store decl b = let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in - let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in + let Sigma (ev, sigma, p) = new_evar_instance nctx sigma (EConstr.of_constr nb) ~principal:true ~store ninst in Sigma (mkNamedLambda_or_LetIn decl ev, sigma, p) end } @@ -206,12 +206,13 @@ let convert_concl ?(check=true) ty k = let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in let conclty = Proofview.Goal.raw_concl gl in + let ty = EConstr.of_constr ty in Refine.refine ~unsafe:true { run = begin fun sigma -> let Sigma ((), sigma, p) = if check then begin let sigma = Sigma.to_evar_map sigma in - ignore (Typing.unsafe_type_of env sigma (EConstr.of_constr ty)); - let sigma,b = Reductionops.infer_conv env sigma ty conclty in + ignore (Typing.unsafe_type_of env sigma ty); + let sigma,b = Reductionops.infer_conv env sigma ty (EConstr.of_constr conclty) in if not b then error "Not convertible."; Sigma.Unsafe.of_pair ((), sigma) end else Sigma.here () sigma in @@ -230,7 +231,7 @@ let convert_hyp ?(check=true) d = let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in Refine.refine ~unsafe:true { run = begin fun sigma -> - Evarutil.new_evar env sigma ~principal:true ~store ty + Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr ty) end } end } @@ -248,8 +249,8 @@ let convert_gen pb x y = Tacticals.New.tclFAIL 0 (str "Not convertible") end } -let convert x y = convert_gen Reduction.CONV x y -let convert_leq x y = convert_gen Reduction.CUMUL x y +let convert x y = convert_gen Reduction.CONV (EConstr.of_constr x) (EConstr.of_constr y) +let convert_leq x y = convert_gen Reduction.CUMUL (EConstr.of_constr x) (EConstr.of_constr y) let clear_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> @@ -300,7 +301,7 @@ let clear_gen fail = function in let env = reset_with_named_context hyps env in let tac = Refine.refine ~unsafe:true { run = fun sigma -> - Evarutil.new_evar env sigma ~principal:true concl + Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr concl) } in Sigma.Unsafe.of_pair (tac, !evdref) end } @@ -330,7 +331,7 @@ let move_hyp id dest = let sign' = move_hyp_in_named_context sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~unsafe:true { run = begin fun sigma -> - Evarutil.new_evar env sigma ~principal:true ~store ty + Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr ty) end } end } @@ -384,7 +385,7 @@ let rename_hyp repl = let nctx = Environ.val_of_named_context nhyps in let instance = List.map (NamedDecl.get_id %> mkVar) hyps in Refine.refine ~unsafe:true { run = begin fun sigma -> - Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance + Evarutil.new_evar_instance nctx sigma (EConstr.of_constr nconcl) ~principal:true ~store instance end } end } @@ -494,7 +495,7 @@ let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Si fun env sigma p -> function | [] -> Sigma ([], sigma, p) | arg :: rem -> - let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in + let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr arg) in let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in Sigma (arg :: rem, sigma, r) @@ -784,35 +785,37 @@ let make_change_arg c pats = { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma } let check_types env sigma mayneedglobalcheck deep newc origc = - let t1 = Retyping.get_type_of env sigma (EConstr.of_constr newc) in + 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 (EConstr.of_constr origc) in + let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma (EConstr.of_constr 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 - isSort (whd_all env sigma (EConstr.of_constr t1)) && - isSort (whd_all env sigma (EConstr.of_constr t2)) + isSort (whd_all env sigma t1) && + isSort (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.") else sigma end else - if not (isSort (whd_all env sigma (EConstr.of_constr t1))) then + if not (isSort (whd_all env sigma t1)) then user_err ~hdr:"convert-check-hyp" (str "Not a type.") else sigma (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun env sigma c -> - let c = EConstr.Unsafe.to_constr c in let Sigma (t', sigma, p) = t.run sigma in let sigma = Sigma.to_evar_map sigma in + let t' = EConstr.of_constr t' in let sigma = check_types env sigma mayneedglobalcheck deep t' c in let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); - Sigma.Unsafe.of_pair (t', sigma) + Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr t', sigma) end } (* Use cumulativity only if changing the conclusion not a subterm *) @@ -1240,8 +1243,8 @@ let cut c = (** Backward compat: normalize [c]. *) let c = if normalize_cut then local_strong whd_betaiota sigma (EConstr.of_constr c) else c in Refine.refine ~unsafe:true { run = begin fun h -> - let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in - let Sigma (x, h, q) = Evarutil.new_evar env h c in + let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (EConstr.of_constr (mkArrow c (Vars.lift 1 concl))) in + let Sigma (x, h, q) = Evarutil.new_evar env h (EConstr.of_constr c) in let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in Sigma (f, h, p +> q) end } @@ -1913,8 +1916,8 @@ let cut_and_apply c = let env = Tacmach.New.pf_env gl in Refine.refine { run = begin fun sigma -> let typ = mkProd (Anonymous, c2, concl) in - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in + let Sigma (f, sigma, p) = Evarutil.new_evar env sigma (EConstr.of_constr typ) in + let Sigma (x, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr c1) in let ans = mkApp (f, [|mkApp (c, [|x|])|]) in Sigma (ans, sigma, p +> q) end } @@ -1983,7 +1986,7 @@ let assumption = if only_eq then (sigma, Constr.equal t concl) else let env = Proofview.Goal.env gl in - infer_conv env sigma t concl + infer_conv env sigma (EConstr.of_constr t) (EConstr.of_constr concl) in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> @@ -2078,7 +2081,7 @@ let clear_body ids = in check <*> Refine.refine ~unsafe:true { run = begin fun sigma -> - Evarutil.new_evar env sigma ~principal:true concl + Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr concl) end } end } @@ -2131,7 +2134,7 @@ let apply_type newcl args = Refine.refine { run = begin fun sigma -> let newcl = nf_betaiota (Sigma.to_evar_map sigma) (EConstr.of_constr newcl) (* As in former Logic.refine *) in let Sigma (ev, sigma, p) = - Evarutil.new_evar env sigma ~principal:true ~store newcl in + Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr newcl) in Sigma (applist (ev, args), sigma, p) end } end } @@ -2151,7 +2154,7 @@ let bring_hyps hyps = let args = Array.of_list (Context.Named.to_instance hyps) in Refine.refine { run = begin fun sigma -> let Sigma (ev, sigma, p) = - Evarutil.new_evar env sigma ~principal:true ~store newcl in + Evarutil.new_evar env sigma ~principal:true ~store (EConstr.of_constr newcl) in Sigma (mkApp (ev, args), sigma, p) end } end } @@ -2677,11 +2680,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in - let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store ccl in + let Sigma (x, sigma, r) = new_evar newenv sigma ~principal:true ~store (EConstr.of_constr ccl) in Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p +> q +> r) | None -> let newenv = insert_before [decl] lastlhyp env in - let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in + let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store (EConstr.of_constr ccl) in Sigma (mkNamedLetIn id c t x, sigma, p) let letin_tac with_eq id c ty occs = @@ -2862,7 +2865,7 @@ let new_generalize_gen_let lconstr = in let tac = Refine.refine { run = begin fun sigma -> - let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in + let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr newcl) in Sigma ((applist (ev, args)), sigma, p) end } in @@ -3549,7 +3552,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = (* Abstract by the extension of the context *) let genctyp = it_mkProd_or_LetIn genarg ctx in (* The goal will become this product. *) - let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true genctyp in + let Sigma (genc, sigma, p) = Evarutil.new_evar env sigma ~principal:true (EConstr.of_constr genctyp) in (* Apply the old arguments giving the proper instantiation of the hyp *) let instc = mkApp (genc, Array.of_list args) in (* Then apply to the original instantiated hyp. *) @@ -3755,7 +3758,7 @@ let specialize_eqs id gl = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar (push_rel_context ctx env) evars t in + let e = e_new_evar (push_rel_context ctx env) evars (EConstr.of_constr t) in aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 26e29540c..1055d28b6 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -193,7 +193,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in nf t in - Pretyping.check_evars env Evd.empty !evars termtype; + Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); let pl, ctx = Evd.universe_context ?names:pl !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry @@ -289,7 +289,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let evm, nf = Evarutil.nf_evar_map_universes !evars in let termtype = nf termtype in let _ = (* Check that the type is free of evars now. *) - Pretyping.check_evars env Evd.empty evm termtype + Pretyping.check_evars env Evd.empty evm (EConstr.of_constr termtype) in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then @@ -363,7 +363,7 @@ let context poly l = let _, ((env', fullctx), impls) = interp_context_evars env evars l in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in let fullctx = Context.Rel.map subst fullctx in - let ce t = Pretyping.check_evars env Evd.empty !evars t in + let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = try named_of_rel_context fullctx diff --git a/toplevel/command.ml b/toplevel/command.ml index c6dd3eb99..dbf256ba8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -618,10 +618,10 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in let pl, uctx = Evd.universe_context ?names:pl evd in - List.iter (check_evars env_params Evd.empty evd) arities; - Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params; + List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; + Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> - List.iter (check_evars env_ar_params Evd.empty evd) ctyps) + List.iter (fun c -> check_evars env_ar_params Evd.empty evd (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) @@ -1031,7 +1031,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = mkApp (Universes.constr_of_global (delayed_force fix_sub_ref), [| argtyp ; wf_rel ; Evarutil.e_new_evar env evdref - ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; + ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) (EConstr.of_constr wf_proof); prop |]) in let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in diff --git a/toplevel/record.ml b/toplevel/record.ml index dc49c5385..929505716 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -163,7 +163,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = Context.Rel.map nf newps in let newfs = Context.Rel.map nf newfs in - let ce t = Pretyping.check_evars env0 Evd.empty evars t in + let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs @@ -364,13 +364,13 @@ let structure_signature ctx = | [decl] -> let env = Environ.empty_named_context_val in let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in + let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in let evm = Sigma.to_evar_map evm in evm | decl::tl -> let env = Environ.empty_named_context_val in let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (RelDecl.get_type decl) in + let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in let evm = Sigma.to_evar_map evm in let new_tl = Util.List.map_i (fun pos decl -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 33b96bc37..01b15407b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -462,7 +462,7 @@ let start_proof_and_print k l hook = let c, _, ctx = Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl (Tacticals.New.tclCOMPLETE tac) - in Evd.set_universe_context sigma ctx, c + in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> error "The statement obligations could not be resolved \ automatically, write a statement definition first." |