aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/classops.ml19
-rw-r--r--pretyping/classops.mli15
-rw-r--r--pretyping/coercion.ml174
-rw-r--r--pretyping/coercion.mli8
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/program.ml3
-rw-r--r--pretyping/program.mli2
-rw-r--r--pretyping/unification.ml2
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/refine.ml2
-rw-r--r--toplevel/class.ml2
12 files changed, 128 insertions, 112 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 882c052f6..96c61647c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -396,7 +396,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
current
else
(evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
- pb.evdref (make_judge current typ) indt).uj_val in
+ pb.evdref (make_judge current typ) (EConstr.of_constr indt)).uj_val in
let sigma = !(pb.evdref) in
(current,try_find_ind pb.env sigma indt names))
| _ -> (current,tmtyp)
@@ -1867,7 +1867,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
let inh_conv_coerce_to_tycon loc env evdref j tycon =
match tycon with
| Some p ->
- let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in
+ let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j (EConstr.of_constr p) in
evdref := evd';
j
| None -> j
@@ -2013,6 +2013,7 @@ let eq_id avoid id =
let hid' = next_ident_away hid avoid in
hid'
+let papp evdref gr args = EConstr.Unsafe.to_constr (papp evdref gr (Array.map EConstr.of_constr args))
let mk_eq evdref typ x y = papp evdref coq_eq_ind [| typ; x ; y |]
let mk_eq_refl evdref typ x = papp evdref coq_eq_refl [| typ; x |]
let mk_JMeq evdref typ x typ' y =
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 753127357..ad43bf322 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -192,14 +192,13 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab
(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)
let find_class_type sigma t =
- let inj = EConstr.Unsafe.to_constr in
let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
match EConstr.kind sigma t' with
- | Var id -> CL_SECVAR id, Univ.Instance.empty, List.map inj args
- | Const (sp,u) -> CL_CONST sp, u, List.map inj args
+ | Var id -> CL_SECVAR id, Univ.Instance.empty, args
+ | Const (sp,u) -> CL_CONST sp, u, args
| Proj (p, c) when not (Projection.unfolded p) ->
- CL_PROJ (Projection.constant p), Univ.Instance.empty, List.map inj (c :: args)
- | Ind (ind_sp,u) -> CL_IND ind_sp, u, List.map inj args
+ CL_PROJ (Projection.constant p), Univ.Instance.empty, (c :: args)
+ | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
| Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
| Sort _ -> CL_SORT, Univ.Instance.empty, []
| _ -> raise Not_found
@@ -231,10 +230,11 @@ let class_of env sigma t =
try
let (cl, u, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
- (EConstr.Unsafe.to_constr t, n1, i, u, args)
+ (t, n1, i, u, args)
with Not_found ->
let t = Tacred.hnf_constr env sigma t in
- let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in
+ let t = EConstr.of_constr t in
+ let (cl, u, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, u, args)
in
@@ -274,11 +274,12 @@ let apply_on_class_of env sigma t cont =
let (cl,u,args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
- EConstr.Unsafe.to_constr t, cont i
+ t, cont i
with Not_found ->
(* Is it worth to be more incremental on the delta steps? *)
let t = Tacred.hnf_constr env sigma t in
- let (cl, u, args) = find_class_type sigma (EConstr.of_constr t) in
+ let t = EConstr.of_constr t in
+ let (cl, u, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
t, cont i
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 4b8a2c1c0..9fb70534f 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -8,6 +8,7 @@
open Names
open Term
+open EConstr
open Evd
open Environ
open Mod_subst
@@ -59,15 +60,15 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
(** [find_class_type env sigma c] returns the head reference of [c],
its universe instance and its arguments *)
-val find_class_type : evar_map -> EConstr.types -> cl_typ * Univ.universe_instance * constr list
+val find_class_type : evar_map -> types -> cl_typ * Univ.universe_instance * constr list
(** raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> EConstr.types -> types * cl_index
+val class_of : env -> evar_map -> types -> types * cl_index
(** raises [Not_found] if not mapped to a class *)
val inductive_class_of : inductive -> cl_index
-val class_args_of : env -> evar_map -> EConstr.types -> constr list
+val class_args_of : env -> evar_map -> types -> constr list
(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
val declare_coercion :
@@ -84,11 +85,11 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
(** @raise Not_found in the following functions when no path exists *)
val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-val lookup_path_between : env -> evar_map -> EConstr.types * EConstr.types ->
+val lookup_path_between : env -> evar_map -> types * types ->
types * types * inheritance_path
-val lookup_path_to_fun_from : env -> evar_map -> EConstr.types ->
+val lookup_path_to_fun_from : env -> evar_map -> types ->
types * inheritance_path
-val lookup_path_to_sort_from : env -> evar_map -> EConstr.types ->
+val lookup_path_to_sort_from : env -> evar_map -> types ->
types * inheritance_path
val lookup_pattern_path_between :
env -> inductive * inductive -> (constructor * int) list
@@ -104,7 +105,7 @@ val install_path_printer :
val string_of_class : cl_typ -> string
val pr_class : cl_typ -> std_ppcmds
val pr_cl_index : cl_index -> std_ppcmds
-val get_coercion_value : coe_index -> constr
+val get_coercion_value : coe_index -> Constr.t
val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_index list
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 90cd3b60b..cc121a96d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -48,29 +48,30 @@ exception NoCoercionNoUnifier of evar_map * unification_error
(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env evd check isproj argl funj =
+ let open EConstr in
let evdref = ref evd in
let rec apply_rec acc typ = function
| [] ->
if isproj then
- let cst = fst (destConst (j_val funj)) in
+ let cst = fst (destConst !evdref (EConstr.of_constr (j_val funj))) in
let p = Projection.make cst false in
let pb = lookup_projection p env in
let args = List.skipn pb.Declarations.proj_npars argl in
let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
- { uj_val = applist (mkProj (p, hd), tl);
- uj_type = typ }
+ { uj_val = EConstr.Unsafe.to_constr (applist (mkProj (p, hd), tl));
+ uj_type = EConstr.Unsafe.to_constr typ }
else
- { uj_val = applist (j_val funj,argl);
- uj_type = typ }
+ { uj_val = EConstr.Unsafe.to_constr (applist (EConstr.of_constr (j_val funj),argl));
+ uj_type = EConstr.Unsafe.to_constr typ }
| h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
- match kind_of_term (whd_all env evd (EConstr.of_constr typ)) with
+ match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
| Prod (_,c1,c2) ->
- if check && not (e_cumul env evdref (EConstr.of_constr (Retyping.get_type_of env evd (EConstr.of_constr h))) (EConstr.of_constr c1)) then
+ if check && not (e_cumul env evdref (EConstr.of_constr (Retyping.get_type_of env !evdref h)) c1) then
raise NoCoercion;
- apply_rec (h::acc) (subst1 h c2) restl
+ apply_rec (h::acc) (Vars.subst1 h c2) restl
| _ -> anomaly (Pp.str "apply_coercion_args")
in
- let res = apply_rec [] funj.uj_type argl in
+ let res = apply_rec [] (EConstr.of_constr funj.uj_type) argl in
!evdref, res
(* appliquer le chemin de coercions de patterns p *)
@@ -92,17 +93,17 @@ 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
- Evarutil.e_new_evar env evdref ~src c
+ EConstr.of_constr (Evarutil.e_new_evar env evdref ~src (EConstr.Unsafe.to_constr c))
let app_opt env evdref f t =
- whd_betaiota !evdref (EConstr.of_constr (app_opt f t))
+ EConstr.of_constr (whd_betaiota !evdref (app_opt f t))
let pair_of_array a = (a.(0), a.(1))
-let disc_subset x =
- match kind_of_term x with
+let disc_subset sigma x =
+ match EConstr.kind sigma x with
| App (c, l) ->
- (match kind_of_term c with
+ (match EConstr.kind sigma c with
Ind (i,_) ->
let len = Array.length l in
let sigty = delayed_force sig_typ in
@@ -120,19 +121,25 @@ let hnf env evd c = whd_all env evd c
let hnf_nodelta env evd c = whd_betaiota evd c
let lift_args n sign =
+ let open EConstr in
let rec liftrec k = function
- | t::sign -> liftn n k t :: (liftrec (k-1) sign)
+ | t::sign -> Vars.liftn n k t :: (liftrec (k-1) sign)
| [] -> []
in
liftrec (List.length sign) sign
+let local_assum (na, t) =
+ let open Context.Rel.Declaration in
+ LocalAssum (na, EConstr.Unsafe.to_constr t)
+
let mu env evdref t =
let rec aux v =
- let v' = hnf env !evdref (EConstr.of_constr v) in
- match disc_subset v' with
+ let v' = hnf env !evdref v in
+ let v' = EConstr.of_constr v' in
+ match disc_subset !evdref v' with
| Some (u, p) ->
let f, ct = aux u in
- let p = hnf_nodelta env !evdref (EConstr.of_constr p) in
+ let p = EConstr.of_constr (hnf_nodelta env !evdref p) in
(Some (fun x ->
app_opt env evdref
f (papp evdref sig_proj1 [| u; p; x |])),
@@ -140,21 +147,25 @@ let mu env evdref t =
| None -> (None, v)
in aux t
-and coerce loc env evdref (x : Term.constr) (y : Term.constr)
- : (Term.constr -> Term.constr) option
+and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr)
+ : (EConstr.constr -> EConstr.constr) option
=
+ let open EConstr in
+ let open Vars in
let open Context.Rel.Declaration in
let rec coerce_unify env x y =
- let x = hnf env !evdref (EConstr.of_constr x) and y = hnf env !evdref (EConstr.of_constr y) in
+ let x = hnf env !evdref x and y = hnf env !evdref y in
+ let x = EConstr.of_constr x in
+ let y = EConstr.of_constr y in
try
- evdref := the_conv_x_leq env (EConstr.of_constr x) (EConstr.of_constr y) !evdref;
+ evdref := the_conv_x_leq env x y !evdref;
None
with UnableToUnify _ -> coerce' env x y
- and coerce' env x y : (Term.constr -> Term.constr) option =
+ and coerce' env x y : (EConstr.constr -> EConstr.constr) option =
let subco () = subset_coerce env evdref x y in
let dest_prod c =
- match Reductionops.splay_prod_n env (!evdref) 1 (EConstr.of_constr c) with
- | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c
+ match Reductionops.splay_prod_n env (!evdref) 1 c with
+ | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na, EConstr.of_constr t), EConstr.of_constr c
| _ -> raise NoSubtacCoercion
in
let coerce_application typ typ' c c' l l' =
@@ -162,7 +173,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let rec aux tele typ typ' i co =
if i < len then
let hdx = l.(i) and hdy = l'.(i) in
- try evdref := the_conv_x_leq env (EConstr.of_constr hdx) (EConstr.of_constr hdy) !evdref;
+ try evdref := the_conv_x_leq env hdx hdy !evdref;
let (n, eqT), restT = dest_prod typ in
let (n', eqT'), restT' = dest_prod typ' in
aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
@@ -170,16 +181,16 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let (n, eqT), restT = dest_prod typ in
let (n', eqT'), restT' = dest_prod typ' in
let _ =
- try evdref := the_conv_x_leq env (EConstr.of_constr eqT) (EConstr.of_constr eqT') !evdref
+ try evdref := the_conv_x_leq env eqT eqT' !evdref
with UnableToUnify _ -> raise NoSubtacCoercion
in
(* Disallow equalities on arities *)
- if Reduction.is_arity env eqT then raise NoSubtacCoercion;
+ if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion;
let restargs = lift_args 1
(List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
in
let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
- let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
+ let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
let evar = make_existential loc env evdref eq in
let eq_app x = papp evdref coq_eq_rect
@@ -188,15 +199,15 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
aux (hdy :: tele) (subst1 hdx restT)
(subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some (fun x ->
- let term = EConstr.of_constr (co x) in
- Typing.e_solve_evars env evdref term)
+ let term = co x in
+ EConstr.of_constr (Typing.e_solve_evars env evdref term))
in
- if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
+ if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
(* Second-order unification needed. *)
raise NoSubtacCoercion;
aux [] typ typ' 0 (fun x -> x)
in
- match (kind_of_term x, kind_of_term y) with
+ match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
| Sort s, Sort s' ->
(match s, s' with
| Prop x, Prop y when x == y -> None
@@ -207,7 +218,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let name' =
Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
in
- let env' = push_rel (LocalAssum (name', a')) env in
+ let env' = push_rel (local_assum (name', a')) env in
let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
let coec1 = app_opt env' evdref c1 (mkRel 1) in
@@ -224,7 +235,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
(mkApp (lift 1 f, [| coec1 |])))))
| App (c, l), App (c', l') ->
- (match kind_of_term c, kind_of_term c' with
+ (match EConstr.kind !evdref c, EConstr.kind !evdref c' with
Ind (i, u), Ind (i', u') -> (* Inductive types *)
let len = Array.length l in
let sigT = delayed_force sigT_typ in
@@ -241,23 +252,21 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
in
let c1 = coerce_unify env a a' in
let remove_head a c =
- match kind_of_term c with
+ match EConstr.kind !evdref c with
| Lambda (n, t, t') -> c, t'
| Evar (k, args) ->
- let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k, Array.map EConstr.of_constr args) in
+ let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,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
- let (domk, args) = destEvar dom in
- evdref := define domk a !evdref;
+ let (n, dom, rng) = destLambda !evdref t in
+ if isEvar !evdref dom then
+ let (domk, args) = destEvar !evdref dom in
+ evdref := define domk (EConstr.Unsafe.to_constr a) !evdref;
else ();
t, rng
| _ -> raise NoSubtacCoercion
in
let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
- let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in
+ let env' = push_rel (local_assum (Name Namegen.default_dependent_ident, a)) env in
let c2 = coerce_unify env' b b' in
match c1, c2 with
| None, None -> None
@@ -297,30 +306,30 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
let evm = !evdref in
(try subco ()
with NoSubtacCoercion ->
- let typ = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
- let typ' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
- coerce_application typ typ' c c' l l')
+ let typ = Typing.unsafe_type_of env evm c in
+ let typ' = Typing.unsafe_type_of env evm c' in
+ coerce_application (EConstr.of_constr typ) (EConstr.of_constr typ') c c' l l')
else
subco ()
- | x, y when Constr.equal c c' ->
+ | x, y when EConstr.eq_constr !evdref c c' ->
if Int.equal (Array.length l) (Array.length l') then
let evm = !evdref in
- let lam_type = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
- let lam_type' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
- coerce_application lam_type lam_type' c c' l l'
+ let lam_type = Typing.unsafe_type_of env evm c in
+ let lam_type' = Typing.unsafe_type_of env evm c' in
+ coerce_application (EConstr.of_constr lam_type) (EConstr.of_constr lam_type') c c' l l'
else subco ()
| _ -> subco ())
| _, _ -> subco ()
and subset_coerce env evdref x y =
- match disc_subset x with
+ match disc_subset !evdref x with
Some (u, p) ->
let c = coerce_unify env u y in
let f x =
app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |])
in Some f
| None ->
- match disc_subset y with
+ match disc_subset !evdref y with
Some (u, p) ->
let c = coerce_unify env x u in
Some
@@ -337,8 +346,8 @@ let app_coercion env evdref coercion v =
match coercion with
| None -> v
| Some f ->
- let v' = Typing.e_solve_evars env evdref (EConstr.of_constr (f v)) in
- whd_betaiota !evdref (EConstr.of_constr v')
+ let v' = Typing.e_solve_evars env evdref (f v) in
+ EConstr.of_constr (whd_betaiota !evdref (EConstr.of_constr v'))
let coerce_itf loc env evd v t c1 =
let evdref = ref evd in
@@ -358,7 +367,7 @@ let apply_coercion env sigma p hj typ_cl =
(fun (ja,typ_cl,sigma) i ->
let ((fv,isid,isproj),ctx) = coercion_value i in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- let argl = (class_args_of env sigma (EConstr.of_constr typ_cl))@[ja.uj_val] in
+ let argl = (class_args_of env sigma typ_cl)@[EConstr.of_constr ja.uj_val] in
let sigma, jres =
apply_coercion_args env sigma true isproj argl fv
in
@@ -366,7 +375,7 @@ let apply_coercion env sigma p hj typ_cl =
{ uj_val = ja.uj_val; uj_type = jres.uj_type }
else
jres),
- jres.uj_type,sigma)
+ EConstr.of_constr jres.uj_type,sigma)
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
@@ -375,7 +384,8 @@ 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 EConstr.kind evd (EConstr.of_constr t) with
+ let t = EConstr.of_constr t in
+ match EConstr.kind evd t with
| Prod (_,_,_) -> (evd,j)
| Evar ev ->
let (evd',t) = Evardefine.define_evar_as_product evd ev in
@@ -389,7 +399,7 @@ let inh_app_fun_core env evd j =
try
let evdref = ref evd in
let coercef, t = mu env evdref t in
- let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
+ let res = { uj_val = EConstr.Unsafe.to_constr (app_opt env evdref coercef (EConstr.of_constr j.uj_val)); uj_type = EConstr.Unsafe.to_constr t } in
(!evdref, res)
with NoSubtacCoercion | NoCoercion ->
(evd,j)
@@ -427,10 +437,10 @@ let inh_coerce_to_sort loc env evd j =
let inh_coerce_to_base loc env evd j =
if Flags.is_program_mode () then
let evdref = ref evd in
- let ct, typ' = mu env evdref j.uj_type in
+ let ct, typ' = mu env evdref (EConstr.of_constr j.uj_type) in
let res =
- { uj_val = app_coercion env evdref ct j.uj_val;
- uj_type = typ' }
+ { uj_val = EConstr.Unsafe.to_constr (app_coercion env evdref ct (EConstr.of_constr j.uj_val));
+ uj_type = EConstr.Unsafe.to_constr typ' }
in !evdref, res
else (evd, j)
@@ -442,33 +452,35 @@ let inh_coerce_to_prod loc env evd t =
else (evd, t)
let inh_coerce_to_fail env evd rigidonly v t c1 =
- if rigidonly && not (Heads.is_rigid env c1 && Heads.is_rigid env t)
+ if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr c1) && Heads.is_rigid env (EConstr.Unsafe.to_constr t))
then
raise NoCoercion
else
let evd, v', t' =
try
- let t2,t1,p = lookup_path_between env evd (EConstr.of_constr t,EConstr.of_constr c1) in
+ let t2,t1,p = lookup_path_between env evd (t,c1) in
match v with
| Some v ->
let evd,j =
apply_coercion env evd p
- {uj_val = v; uj_type = t} t2 in
- evd, Some j.uj_val, j.uj_type
+ {uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr t} t2 in
+ evd, Some (EConstr.of_constr j.uj_val), (EConstr.of_constr j.uj_type)
| None -> evd, None, t
with Not_found -> raise NoCoercion
in
- try (the_conv_x_leq env (EConstr.of_constr t') (EConstr.of_constr c1) evd, v')
+ try (the_conv_x_leq env t' c1 evd, v')
with UnableToUnify _ -> raise NoCoercion
let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
- try (the_conv_x_leq env (EConstr.of_constr t) (EConstr.of_constr c1) evd, v)
+ let open EConstr in
+ let open Vars in
+ try (the_conv_x_leq env t c1 evd, v)
with UnableToUnify (best_failed_evd,e) ->
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
- kind_of_term (whd_all env evd (EConstr.of_constr t)),
- kind_of_term (whd_all env evd (EConstr.of_constr c1))
+ EConstr.kind evd (EConstr.of_constr (whd_all env evd t)),
+ EConstr.kind evd (EConstr.of_constr (whd_all env evd c1))
with
| Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
@@ -481,16 +493,16 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
| Anonymous -> Name Namegen.default_dependent_ident
| _ -> name in
let open Context.Rel.Declaration in
- let env1 = push_rel (LocalAssum (name,u1)) env in
+ let env1 = push_rel (local_assum (name,u1)) env in
let (evd', v1) =
inh_conv_coerce_to_fail loc env1 evd rigidonly
(Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
let v1 = Option.get v1 in
- let v2 = Option.map (fun v -> beta_applist evd' (EConstr.of_constr (lift 1 v),[EConstr.of_constr v1])) v in
+ let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in
let t2 = match v2 with
- | None -> subst_term evd' (EConstr.of_constr v1) (EConstr.of_constr t2)
+ | None -> subst_term evd' v1 t2
| Some v2 -> Retyping.get_type_of env1 evd' (EConstr.of_constr v2) in
- let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
+ let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly (Option.map EConstr.of_constr v2) (EConstr.of_constr t2) u2 in
(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
| _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
@@ -498,27 +510,27 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
let (evd', val') =
try
- inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+ inh_conv_coerce_to_fail loc env evd rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
with NoCoercionNoUnifier (best_failed_evd,e) ->
try
if Flags.is_program_mode () then
- coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
+ coerce_itf loc env evd (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
else raise NoSubtacCoercion
with
| NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
- error_actual_type ~loc env best_failed_evd cj t e
+ error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
| NoSubtacCoercion ->
let evd' = saturate_evd env evd in
try
if evd' == evd then
- error_actual_type ~loc env best_failed_evd cj t e
+ error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
else
- inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
+ inh_conv_coerce_to_fail loc env evd' rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
with NoCoercionNoUnifier (_evd,_error) ->
- error_actual_type ~loc env best_failed_evd cj t e
+ error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
in
let val' = match val' with Some v -> v | None -> assert(false) in
- (evd',{ uj_val = val'; uj_type = t })
+ (evd',{ uj_val = EConstr.Unsafe.to_constr val'; uj_type = EConstr.Unsafe.to_constr t })
let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 68f9a2e68..62d4fb004 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -36,7 +36,7 @@ val inh_coerce_to_base : Loc.t ->
(** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
val inh_coerce_to_prod : Loc.t ->
- env -> evar_map -> types -> evar_map * types
+ env -> evar_map -> EConstr.types -> evar_map * EConstr.types
(** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an
object of type [t]; i.e. it inserts a coercion into [j], if needed, in such
@@ -44,16 +44,16 @@ val inh_coerce_to_prod : Loc.t ->
applicable. resolve_tc=false disables resolving type classes (as the last
resort before failing) *)
val inh_conv_coerce_to : bool -> Loc.t ->
- env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment
val inh_conv_coerce_rigid_to : bool -> Loc.t ->
- env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
+ env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment
(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
is coercible to an object of type [t'] adding evar constraints if needed;
it fails if no coercion exists *)
val inh_conv_coerces_to : Loc.t ->
- env -> evar_map -> types -> types -> evar_map
+ env -> evar_map -> EConstr.types -> EConstr.types -> evar_map
(** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 28ba60812..18731f1e9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -359,7 +359,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 t
+ evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j (EConstr.of_constr t)
let check_instance loc subst = function
| [] -> ()
@@ -770,8 +770,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 ty in
- evd, 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'))
evdref tycon
in
let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 4b6137b53..2606d91f3 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -29,8 +29,9 @@ let init_constant dir s () = coq_constant "Program" dir s
let init_reference dir s () = coq_reference "Program" dir s
let papp evdref r args =
+ let open EConstr in
let gr = delayed_force r in
- mkApp (Evarutil.e_new_global evdref gr, args)
+ mkApp (EConstr.of_constr (Evarutil.e_new_global evdref gr), args)
let sig_typ = init_reference ["Init"; "Specif"] "sig"
let sig_intro = init_reference ["Init"; "Specif"] "exist"
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 023ff8ca5..64c4ca2c2 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -36,7 +36,7 @@ val mk_coq_and : constr list -> constr
val mk_coq_not : constr -> constr
(** Polymorphic application of delayed references *)
-val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
+val papp : Evd.evar_map ref -> (unit -> global_reference) -> EConstr.constr array -> EConstr.constr
val get_proofs_transparency : unit -> bool
val is_program_cases : unit -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 786cfd31f..b568dd044 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1225,7 +1225,7 @@ let is_mimick_head ts f =
let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
- let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
+ let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j (EConstr.of_constr tycon) in
let evd' = Evarconv.consider_remaining_unif_problems env evd' in
let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
(evd',j'.uj_val)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c2130a64a..0515e4198 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -670,7 +670,7 @@ let define_with_type sigma env ev c =
let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let j = Environ.make_judge c ty in
- let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+ let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
let (ev, _) = destEvar ev in
let sigma = Evd.define ev j.Environ.uj_val sigma in
sigma
diff --git a/proofs/refine.ml b/proofs/refine.ml
index b62f0bea4..19134bfa3 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -136,7 +136,7 @@ let with_type env evd c t =
let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in
let j = Environ.make_judge c my_type in
let (evd,j') =
- Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+ Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t)
in
evd , j'.Environ.uj_val
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6295eb336..46b212dee 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -85,7 +85,7 @@ let uniform_cond nargs lt =
let rec aux = function
| (0,[]) -> true
| (n,t::l) ->
- let t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) in
+ let t = strip_outer_cast Evd.empty t (** FIXME *) in
isRel t && Int.equal (destRel t) n && aux ((n-1),l)
| _ -> false
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:27:30 +0000