aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/cases.ml8
-rw-r--r--pretyping/coercion.ml11
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evardefine.ml65
-rw-r--r--pretyping/evardefine.mli12
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/pretype_errors.mli8
-rw-r--r--pretyping/pretyping.ml20
-rw-r--r--pretyping/typing.ml21
-rw-r--r--pretyping/unification.ml11
-rw-r--r--toplevel/himsg.ml4
11 files changed, 88 insertions, 78 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4dd502106..915cd261d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -336,7 +336,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
let find_tomatch_tycon evdref env loc = function
(* Try if some 'in I ...' is present and can be used as a constraint *)
| Some (_,ind,realnal) ->
- mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal)
+ mk_tycon (EConstr.of_constr (inductive_template evdref env loc ind)),Some (List.rev realnal)
| None ->
empty_tycon,None
@@ -1211,7 +1211,7 @@ let rec generalize_problem names pb = function
(* No more patterns: typing the right-hand side of equations *)
let build_leaf pb =
let rhs = extract_rhs pb in
- let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in
+ let j = pb.typing_function (mk_tycon (EConstr.of_constr pb.pred)) rhs.rhs_env pb.evdref rhs.it in
j_nf_evar !(pb.evdref) j
(* Build the sub-pattern-matching problem for a given branch "C x1..xn as x" *)
@@ -1972,7 +1972,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let envar = List.fold_right push_rel_context arsign env in
let sigma, newt = new_sort_variable univ_flexible_alg sigma in
let evdref = ref sigma in
- let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
+ let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in
let sigma = !evdref in
let predccl = (j_nf_evar sigma predcclj).uj_val in
[sigma, predccl]
@@ -2238,7 +2238,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
eqs_rels @ neqs_rels @ rhs_rels', arity
in
let rhs_env = push_rel_context rhs_rels' env in
- let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
+ let j = typing_fun (mk_tycon (EConstr.of_constr tycon)) rhs_env eqn.rhs.it in
let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6a7f90463..c5418d22e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -244,8 +244,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
match kind_of_term c with
| Lambda (n, t, t') -> c, t'
| Evar (k, args) ->
- let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
+ let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k, Array.map EConstr.of_constr args) in
evdref := evs;
+ let t = EConstr.Unsafe.to_constr t in
let (n, dom, rng) = destLambda t in
let dom = whd_evar !evdref dom in
if isEvar dom then
@@ -374,11 +375,11 @@ let apply_coercion env sigma p hj typ_cl =
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
let t = whd_all env evd (EConstr.of_constr j.uj_type) in
- match kind_of_term t with
+ match EConstr.kind evd (EConstr.of_constr t) with
| Prod (_,_,_) -> (evd,j)
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product evd ev in
- (evd',{ uj_val = j.uj_val; uj_type = t })
+ (evd',{ uj_val = j.uj_val; uj_type = EConstr.Unsafe.to_constr t })
| _ ->
try let t,p =
lookup_path_to_fun_from env evd j.uj_type in
@@ -415,9 +416,9 @@ let inh_tosort_force loc env evd j =
let inh_coerce_to_sort loc env evd j =
let typ = whd_all env evd (EConstr.of_constr j.uj_type) in
- match kind_of_term typ with
+ match EConstr.kind evd (EConstr.of_constr typ) with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
- | Evar ev when not (is_defined evd (fst ev)) ->
+ | Evar ev ->
let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
(evd',{ utj_val = j.uj_val; utj_type = s })
| _ ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 47db71cc6..4540af28b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -503,7 +503,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let i,tF =
if isRel tR || isVar tR then
(* Optimization so as to generate candidates *)
- let i,ev = evar_absorb_arguments env i ev (List.map EConstr.Unsafe.to_constr lF) in
+ let i,ev = evar_absorb_arguments env i (fst ev, Array.map EConstr.of_constr (snd ev)) lF in
i,mkEvar ev
else
i,zip evd apprF in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 3982edd1c..8026ff3e4 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -61,13 +61,13 @@ type val_constraint = constr option
let empty_tycon = None
(* Builds a type constraint *)
-let mk_tycon ty = Some ty
+let mk_tycon ty = Some (EConstr.Unsafe.to_constr ty)
(* Constrains the value of a type *)
let empty_valcon = None
(* Builds a value constraint *)
-let mk_valcon c = Some c
+let mk_valcon c = Some (EConstr.Unsafe.to_constr c)
let idx = Namegen.default_dependent_ident
@@ -75,11 +75,12 @@ let idx = Namegen.default_dependent_ident
let define_pure_evar_as_product evd evk =
let open Context.Named.Declaration in
+ let open EConstr in
let evi = Evd.find_undefined evd evk in
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 concl in
+ let s = destSort evd (EConstr.of_constr 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
@@ -103,20 +104,21 @@ let define_pure_evar_as_product evd evk =
let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
evd3, rng
in
- let prod = mkProd (Name id, dom, subst_var id rng) in
- let evd3 = Evd.define evk prod evd2 in
+ let prod = mkProd (Name id, EConstr.of_constr dom, EConstr.of_constr (subst_var id rng)) in
+ let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in
evd3,prod
(* Refine an applied evar to a product and returns its instantiation *)
let define_evar_as_product evd (evk,args) =
+ let open EConstr in
let evd,prod = define_pure_evar_as_product evd evk in
(* Quick way to compute the instantiation of evk with args *)
- let na,dom,rng = destProd prod in
- let evdom = mkEvar (fst (destEvar dom), args) in
- let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
- let evrng = mkEvar (fst (destEvar rng), evrngargs) in
- evd,mkProd (na, evdom, evrng)
+ let na,dom,rng = destProd evd prod in
+ let evdom = mkEvar (fst (destEvar evd dom), args) in
+ let evrngargs = Array.cons (mkRel 1) (Array.map (Vars.lift 1) args) in
+ let evrng = mkEvar (fst (destEvar evd rng), evrngargs) in
+ evd, mkProd (na, evdom, evrng)
(* Refine an evar with an abstraction
@@ -129,38 +131,42 @@ let define_evar_as_product evd (evk,args) =
let define_pure_evar_as_lambda env evd evk =
let open Context.Named.Declaration in
+ let open EConstr in
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
- let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in
- let evd1,(na,dom,rng) = match kind_of_term typ with
+ let typ = EConstr.of_constr (Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi))) in
+ let evd1,(na,dom,rng) = match EConstr.kind evd typ with
| Prod (na,dom,rng) -> (evd,(na,dom,rng))
- | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
+ | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
| _ -> error_not_product env evd typ in
let avoid = ids_of_named_context (evar_context evi) in
+ let dom = EConstr.Unsafe.to_constr dom in
let id =
next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
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 (subst1 (mkVar id) rng) ~filter in
- let lam = mkLambda (Name id, dom, subst_var id body) in
- Evd.define evk lam evd2, lam
+ let evd2,body = new_evar_unsafe newenv evd1 ~src (EConstr.Unsafe.to_constr (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
let define_evar_as_lambda env evd (evk,args) =
+ let open EConstr in
let evd,lam = define_pure_evar_as_lambda env evd evk in
(* Quick way to compute the instantiation of evk with args *)
- let na,dom,body = destLambda lam in
- let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
- let evbody = mkEvar (fst (destEvar body), evbodyargs) in
- evd,mkLambda (na, dom, evbody)
+ let na,dom,body = destLambda evd lam in
+ let evbodyargs = Array.cons (mkRel 1) (Array.map (Vars.lift 1) args) in
+ let evbody = mkEvar (fst (destEvar evd body), evbodyargs) in
+ evd, mkLambda (na, dom, evbody)
let rec evar_absorb_arguments env evd (evk,args as ev) = function
- | [] -> evd,ev
+ | [] -> evd, (evk, Array.map EConstr.Unsafe.to_constr args)
| a::l ->
+ let open EConstr in
(* TODO: optimize and avoid introducing intermediate evars *)
let evd,lam = define_pure_evar_as_lambda env evd evk in
- let _,_,body = destLambda lam in
- let evk = fst (destEvar body) in
+ let _,_,body = destLambda evd lam in
+ let evk = fst (destEvar evd body) in
evar_absorb_arguments env evd (evk, Array.cons a args) l
(* Refining an evar to a sort *)
@@ -180,23 +186,24 @@ let define_evar_as_sort env evd (ev,args) =
an evar instantiate it with the product of 2 new evars. *)
let split_tycon loc env evd tycon =
+ let open EConstr in
let rec real_split evd c =
- let t = Reductionops.whd_all env evd (EConstr.of_constr c) in
- match kind_of_term t with
+ let t = Reductionops.whd_all env evd c in
+ match EConstr.kind evd (EConstr.of_constr t) with
| Prod (na,dom,rng) -> evd, (na, dom, rng)
| Evar ev (* ev is undefined because of whd_all *) ->
let (evd',prod) = define_evar_as_product evd ev in
- let (_,dom,rng) = destProd prod in
+ let (_,dom,rng) = destProd evd prod in
evd',(Anonymous, dom, rng)
- | App (c,args) when isEvar c ->
- let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
+ | App (c,args) when isEvar evd c ->
+ let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in
real_split evd' (mkApp (lam,args))
| _ -> error_not_product ~loc env evd c
in
match tycon with
| None -> evd,(Anonymous,None,None)
| Some c ->
- let evd', (n, dom, rng) = real_split evd c in
+ let evd', (n, dom, rng) = real_split evd (EConstr.of_constr c) in
evd', (n, mk_tycon dom, mk_tycon rng)
let valcon_of_tycon x = x
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index 07b0e69d9..f6d0efba6 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -18,15 +18,15 @@ type type_constraint = types option
type val_constraint = constr option
val empty_tycon : type_constraint
-val mk_tycon : constr -> type_constraint
+val mk_tycon : EConstr.constr -> type_constraint
val empty_valcon : val_constraint
-val mk_valcon : constr -> val_constraint
+val mk_valcon : EConstr.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 -> existential -> constr list ->
+val evar_absorb_arguments : env -> evar_map -> EConstr.existential -> EConstr.constr list ->
evar_map * existential
val split_tycon :
@@ -36,9 +36,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 -> 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
+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
(** {6 debug pretty-printer:} *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f8f6d44bf..f28fb84ba 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -44,14 +44,14 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+ | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr
(* Pretyping *)
| VarNotFound of Id.t
| UnexpectedType of constr * constr
- | NotProduct of constr
+ | NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
| UnsatisfiableConstraints of
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index b015add79..8a6d8b6b3 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -45,14 +45,14 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+ | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr
(** Pretyping *)
| VarNotFound of Id.t
| UnexpectedType of constr * constr
- | NotProduct of constr
+ | NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
| UnsatisfiableConstraints of
@@ -110,7 +110,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
- constr -> constr list -> (env * type_error) option -> 'b
+ constr -> EConstr.constr list -> (env * type_error) option -> 'b
val error_wrong_abstraction_type : env -> Evd.evar_map ->
Name.t -> constr -> types -> types -> 'b
@@ -132,7 +132,7 @@ val error_unexpected_type :
?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
val error_not_product :
- ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
+ ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
(** {6 Error in conversion from AST to glob_constr } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3c48c42df..b689bb7c7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -606,7 +606,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl
| (na,bk,Some bd,ty)::bl ->
let ty' = pretype_type empty_valcon env evdref lvar ty in
- let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
+ let bd' = pretype (mk_tycon (EConstr.of_constr ty'.utj_val)) env evdref lvar bd in
let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
@@ -640,7 +640,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
decompose_prod_n_assum (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in
let nenv = push_rel_context ctxt newenv in
- let j = pretype (mk_tycon ty) nenv evdref lvar def 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 })
ctxtv vdef in
@@ -815,7 +815,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
match c1 with
| GCast (loc, c, CastConv t) ->
let tj = pretype_type empty_valcon env evdref lvar t in
- pretype (mk_tycon tj.utj_val) env evdref lvar c
+ pretype (mk_tycon (EConstr.of_constr tj.utj_val)) env evdref lvar c
| _ -> pretype empty_tycon env evdref lvar c1
in
let t = evd_comb1 (Evarsolve.refresh_universes
@@ -895,7 +895,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
@[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 fj = pretype (mk_tycon fty) env_f evdref lvar d 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 cj.uj_val p;
@@ -973,7 +973,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
cs.cs_args
in
let env_c = push_rel_context csgn env in
- let bj = pretype (mk_tycon pi) env_c evdref lvar b 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
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
@@ -1028,7 +1028,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
(ConversionFailed (env.ExtraEnv.env,cty,tval))
end
| _ ->
- pretype (mk_tycon tval) env evdref lvar c, tval
+ pretype (mk_tycon (EConstr.of_constr tval)) env evdref lvar c, tval
in
let v = mkCast (cj.uj_val, k, tval) in
{ uj_val = v; uj_type = tval }
@@ -1041,7 +1041,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
let c, update =
try
let c = List.assoc id update in
- let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c 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
with Not_found ->
try
@@ -1068,9 +1068,9 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
let s =
let sigma = !evdref in
let t = Retyping.get_type_of env.ExtraEnv.env sigma (EConstr.of_constr v) in
- match kind_of_term (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t)) with
+ 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 ev) ->
+ | Evar ev when is_Type (existential_type sigma (fst ev, Array.map EConstr.Unsafe.to_constr (snd 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
@@ -1101,7 +1101,7 @@ 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 exptyp) env evdref lvar c).uj_val
+ (pretype k0 flags.use_typeclasses (mk_tycon (EConstr.of_constr exptyp)) env evdref lvar c).uj_val
| IsType ->
(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val
in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index acfe05f24..db31541cd 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl =
Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
let e_type_judgment env evdref j =
- match kind_of_term (whd_all env !evdref (EConstr.of_constr j.uj_type)) with
+ match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
| Sort s -> {utj_val = j.uj_val; utj_type = s }
| Evar ev ->
let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -49,26 +49,27 @@ let e_assumption_of_judgment env evdref j =
error_assumption env j
let e_judge_of_apply env evdref funj argjv =
+ let open EConstr in
let rec apply_rec n typ = function
| [] ->
- { uj_val = mkApp (j_val funj, Array.map j_val argjv);
- uj_type = typ }
+ { uj_val = Constr.mkApp (j_val funj, Array.map j_val argjv);
+ uj_type = EConstr.Unsafe.to_constr typ }
| hj::restjl ->
- match kind_of_term (whd_all env !evdref (EConstr.of_constr typ)) with
+ match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
| Prod (_,c1,c2) ->
- if Evarconv.e_cumul env evdref hj.uj_type c1 then
- apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+ if Evarconv.e_cumul env evdref hj.uj_type (EConstr.Unsafe.to_constr c1) then
+ apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
else
- error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv
+ error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
evdref := evd';
- let (_,_,c2) = destProd t in
- apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+ let (_,_,c2) = destProd evd' t in
+ apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
| _ ->
error_cant_apply_not_functional env funj argjv
in
- apply_rec 1 funj.uj_type (Array.to_list argjv)
+ apply_rec 1 (EConstr.of_constr funj.uj_type) (Array.to_list argjv)
let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
if not (Int.equal (Array.length lfj) (Array.length explft)) then
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8865e69ef..f282ec4f1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -105,26 +105,27 @@ let abstract_list_all env evd typ c l =
try Typing.type_of env evd p
with
| UserError _ ->
- error_cannot_find_well_typed_abstraction env evd p l None
+ error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) None
| Type_errors.TypeError (env',x) ->
- error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
+ error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) (Some (env',x)) in
evd,(p,typp)
let set_occurrences_of_last_arg args =
Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
let abstract_list_all_with_dependencies env evd typ c l =
+ let open EConstr in
let evd = Sigma.Unsafe.of_evar_map evd in
let Sigma (ev, evd, _) = new_evar env evd typ in
let evd = Sigma.to_evar_map evd in
- let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
+ let evd,ev' = evar_absorb_arguments env evd (destEvar evd (EConstr.of_constr ev)) l in
let n = List.length l in
let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
let evd,b =
Evarconv.second_order_matching empty_transparent_state
env evd ev' argoccs c in
if b then
- let p = nf_evar evd (existential_value evd (destEvar ev)) in
+ let p = nf_evar evd ev in
evd, p
else error_cannot_find_well_typed_abstraction env evd
(nf_evar evd c) l None
@@ -1899,7 +1900,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 oplist in
+ let evd, pred = abstract_list_all_with_dependencies env evd 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/toplevel/himsg.ml b/toplevel/himsg.ml
index 4cffbee82..c09bf59ce 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -405,7 +405,7 @@ let explain_unexpected_type env sigma actual_type expected_type =
str "where" ++ spc () ++ prexp ++ str " was expected."
let explain_not_product env sigma c =
- let c = Evarutil.nf_evar sigma c in
+ let c = EConstr.to_constr sigma c in
let pr = pr_lconstr_env env sigma c in
str "The type of this term is a product" ++ spc () ++
str "while it is expected to be" ++
@@ -654,7 +654,7 @@ let explain_cannot_unify_binding_type env sigma m n =
let explain_cannot_find_well_typed_abstraction env sigma p l e =
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
- hov 0 (pr_enum (pr_lconstr_env env sigma) l) ++ spc () ++
+ hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++
spc () ++ str "which is ill-typed." ++
(match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 12:16:55 +0000