aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/evardefine.ml19
-rw-r--r--pretyping/evardefine.mli15
-rw-r--r--pretyping/evarsolve.ml3
-rw-r--r--pretyping/nativenorm.ml2
-rw-r--r--pretyping/pretyping.ml285
-rw-r--r--pretyping/pretyping.mli8
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli8
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/unification.ml16
13 files changed, 207 insertions, 167 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1a181202c7..92bd1e3895 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 cc121a96de..b9f14aa43c 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 cdcb993b5e..683b33b89f 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 f372dbf066..ff40a69381 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 f7bf4636b9..9c03a6e3f1 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 8a22aed2f2..3bcea4cee5 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 c8bcae0c85..ff3424c44b 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 18731f1e90..cac31a1c57 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 e09648ec3b..603b9f9ea8 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 69d47e8e69..0b97cd253b 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 911dab0b67..5e6a40786c 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 b729f3b9bc..5b8eaa50b1 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 b568dd044e..70aa0be6bd 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)],[])
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 17:41:35 +0000