aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-11-11 15:39:01 +0100
committerPierre-Marie Pédrot2017-02-14 17:27:33 +0100
commit536026f3e20f761e8ef366ed732da7d3b626ac5e (patch)
tree571e44e2277b6d045d6c11fafca58b5ea6e43afa
parentca993b9e7765ac58f70740818758457c9367b0da (diff)
Cleaning up opening of the EConstr module in pretyping folder.
Diffstat
-rw-r--r--plugins/extraction/extraction.ml1
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/coercion.ml11
-rw-r--r--pretyping/constr_matching.ml8
-rw-r--r--pretyping/detyping.ml1
-rw-r--r--pretyping/evarconv.ml49
-rw-r--r--pretyping/evardefine.ml27
-rw-r--r--pretyping/evarsolve.ml79
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--pretyping/reductionops.ml100
-rw-r--r--pretyping/retyping.ml19
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/tacred.ml47
-rw-r--r--pretyping/typing.ml7
-rw-r--r--pretyping/unification.ml28
-rw-r--r--tactics/tactics.ml2
16 files changed, 135 insertions, 249 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0c4fa70555..6559aeb082 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -599,6 +599,7 @@ let rec extract_term env mle mlt c args =
extract_cons_app env mle mlt cp args
| Proj (p, c) ->
let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in
+ let term = EConstr.Unsafe.to_constr term in
extract_term env mle mlt term args
| Rel n ->
(* As soon as the expected [mlt] for the head is known, *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b43e2193af..57d12a19f6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -111,7 +111,6 @@ let make_anonymous_patvars n =
let relocate_rel n1 n2 k j = if Int.equal j (n1 + k) then n2+k else j
let rec relocate_index sigma n1 n2 k t =
- let open EConstr in
match EConstr.kind sigma t with
| Rel j when Int.equal j (n1 + k) -> mkRel (n2+k)
| Rel j when j < n1+k -> t
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2d4296fe4f..e7279df7a5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -18,6 +18,7 @@ open CErrors
open Util
open Names
open Term
+open EConstr
open Vars
open Reductionops
open Environ
@@ -48,7 +49,6 @@ 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
| [] ->
@@ -68,7 +68,7 @@ let apply_coercion_args env evd check isproj argl funj =
| Prod (_,c1,c2) ->
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) (Vars.subst1 h c2) restl
+ apply_rec (h::acc) (subst1 h c2) restl
| _ -> anomaly (Pp.str "apply_coercion_args")
in
let res = apply_rec [] funj.uj_type argl in
@@ -121,9 +121,8 @@ 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 -> Vars.liftn n k t :: (liftrec (k-1) sign)
+ | t::sign -> liftn n k t :: (liftrec (k-1) sign)
| [] -> []
in
liftrec (List.length sign) sign
@@ -150,8 +149,6 @@ let mu env evdref t =
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 x and y = hnf env !evdref y in
@@ -478,8 +475,6 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
with UnableToUnify _ -> raise NoCoercion
let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
- 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
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ecf6b11219..4d2500ccd6 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -238,7 +238,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
match EConstr.kind sigma c2 with
| Proj (pr, c) when not (Projection.unfolded pr) ->
(try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
- sorec ctx env subst p (EConstr.of_constr term)
+ sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| _ -> raise PatternMatchingFailure)
@@ -254,7 +254,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
else raise PatternMatchingFailure
| _, Proj (pr,c) when not (Projection.unfolded pr) ->
(try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
- sorec ctx env subst p (EConstr.of_constr term)
+ sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| _, _ ->
try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
@@ -266,7 +266,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PApp (c, args), Proj (pr, c2) ->
(try let term = Retyping.expand_projection env sigma pr c2 [] in
- sorec ctx env subst p (EConstr.of_constr term)
+ sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
@@ -460,7 +460,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
if partial_app then
try
let term = Retyping.expand_projection env sigma p c' [] in
- aux env (EConstr.of_constr term) mk_ctx next
+ aux env term mk_ctx next
with Retyping.RetypeError _ -> next ()
else
try_aux [env, c'] next_mk_ctx next
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e5e778f23a..4756ec30e7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -513,6 +513,7 @@ let rec detype flags avoid env sigma t =
if print_primproj_params () then
try
let c = Retyping.expand_projection (snd env) sigma p (EConstr.of_constr c) [] in
+ let c = EConstr.Unsafe.to_constr c in
detype flags avoid env sigma c
with Retyping.RetypeError _ -> noparams ()
else noparams ()
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 639d6260ea..77e91095fc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,15 +6,18 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module CVars = Vars
+
open CErrors
open Util
open Names
open Term
+open Termops
+open EConstr
open Vars
open CClosure
open Reduction
open Reductionops
-open Termops
open Environ
open Recordops
open Evarutil
@@ -43,14 +46,12 @@ let _ = Goptions.declare_bool_option {
}
let unfold_projection env evd ts p c =
- let open EConstr in
let cst = Projection.constant p in
if is_transparent_constant ts cst then
Some (mkProj (Projection.make cst true, c))
else None
let eval_flexible_term ts env evd c =
- let open EConstr in
match EConstr.kind evd c with
| Const (c,u as cu) ->
if is_transparent_constant ts c
@@ -59,7 +60,7 @@ let eval_flexible_term ts env evd c =
| Rel n ->
(try match lookup_rel n env with
| RelDecl.LocalAssum _ -> None
- | RelDecl.LocalDef (_,v,_) -> Some (Vars.lift n (EConstr.of_constr v))
+ | RelDecl.LocalDef (_,v,_) -> Some (lift n (EConstr.of_constr v))
with Not_found -> None)
| Var id ->
(try
@@ -67,7 +68,7 @@ let eval_flexible_term ts env evd c =
Option.map EConstr.of_constr (env |> lookup_named id |> NamedDecl.get_value)
else None
with Not_found -> None)
- | LetIn (_,b,_,c) -> Some (Vars.subst1 b c)
+ | LetIn (_,b,_,c) -> Some (subst1 b c)
| Lambda _ -> Some c
| Proj (p, c) ->
if Projection.unfolded p then assert false
@@ -105,7 +106,6 @@ let position_problem l2r = function
| CUMUL -> Some l2r
let occur_rigidly (evk,_ as ev) evd t =
- let open EConstr in
let rec aux t =
match EConstr.kind evd t with
| App (f, c) -> if aux f then Array.exists aux c else false
@@ -141,14 +141,13 @@ let occur_rigidly (evk,_ as ev) evd t =
projection would have been reduced) *)
let check_conv_record env sigma (t1,sk1) (t2,sk2) =
- let open EConstr in
let (proji, u), arg = Termops.global_app_of_constr sigma t1 in
let canon_s,sk2_effective =
try
match EConstr.kind sigma t2 with
Prod (_,a,b) -> (* assert (l2=[]); *)
let _, a, b = destProd sigma t2 in
- if Vars.noccurn sigma 1 b then
+ if noccurn sigma 1 b then
lookup_canonical_conversion (proji, Prod_cs),
(Stack.append_app [|a;EConstr.of_constr (pop b)|] Stack.empty)
else raise Not_found
@@ -185,9 +184,9 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
| None -> raise Not_found
| Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
- let c' = EConstr.of_constr (subst_univs_level_constr subst c) in
- let t' = subst_univs_level_constr subst t' in
- let bs' = List.map (subst_univs_level_constr subst %> EConstr.of_constr) bs in
+ let c' = EConstr.of_constr (CVars.subst_univs_level_constr subst c) in
+ let t' = CVars.subst_univs_level_constr subst t' in
+ let bs' = List.map (CVars.subst_univs_level_constr subst %> EConstr.of_constr) bs in
let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in
ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
@@ -379,7 +378,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
- let open EConstr in
let quick_fail i = (* not costly, loses info *)
UnifFailure (i, NotSameHead)
in
@@ -466,7 +464,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let termM' = Retyping.expand_projection env evd p c [] in
let apprM', cstsM' =
whd_betaiota_deltazeta_for_iota_state
- (fst ts) env evd cstsM (EConstr.of_constr termM',skM)
+ (fst ts) env evd cstsM (termM',skM)
in
let delta' i =
switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM')
@@ -642,7 +640,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Catch the p.c ~= p c' cases *)
| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
let res =
- try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c [])))
+ try Some (destApp evd (Retyping.expand_projection env evd p c []))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -653,7 +651,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
let res =
- try Some (destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' [])))
+ try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -699,7 +697,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Lambda _ -> assert (match args with [] -> true | _ -> false); true
| LetIn (_,b,_,c) -> is_unnamed
(fst (whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i Cst_stack.empty (EConstr.Vars.subst1 b c, args)))
+ (fst ts) env i Cst_stack.empty (subst1 b c, args)))
| Fix _ -> true (* Partially applied fix can be the result of a whd call *)
| Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
| Case _ | App _| Cast _ -> assert false in
@@ -878,7 +876,6 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
had to be initially resolved
*)
- let open EConstr in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
if Reductionops.Stack.compare_shape sk1 sk2 then
let (evd',ks,_,test) =
@@ -886,12 +883,12 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
(fun (i,ks,m,test) b ->
if match n with Some n -> Int.equal m n | None -> false then
let ty = EConstr.of_constr (Retyping.get_type_of env i t2) in
- let test i = evar_conv_x trs env i CUMUL ty (Vars.substl ks b) in
+ let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
(i,t2::ks, m-1, test)
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 (Vars.substl ks b) in
+ let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (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
@@ -900,17 +897,17 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
ise_and evd'
[(fun i ->
exact_ise_stack2 env i
- (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (Vars.substl ks x))
+ (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
params1 params);
(fun i ->
exact_ise_stack2 env i
- (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (Vars.substl ks u))
+ (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
us2 us);
(fun i -> evar_conv_x trs env i CONV c1 app);
(fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
test;
(fun i -> evar_conv_x trs env i CONV h2
- (EConstr.of_constr (fst (decompose_app_vect i (Vars.substl ks h)))))]
+ (EConstr.of_constr (fst (decompose_app_vect i (substl ks h)))))]
else UnifFailure(evd,(*dummy*)NotSameHead)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
@@ -951,7 +948,6 @@ let set_evar_conv f = Hook.set evar_conv_hook_set f
(* We assume here |l1| <= |l2| *)
let first_order_unification ts env evd (ev1,l1) (term2,l2) =
- let open EConstr in
let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in
ise_and evd
(* First compare extra args for better failure message *)
@@ -973,7 +969,6 @@ let choose_less_dependent_instance evk evd term args =
| (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd)
let apply_on_subterm env evdref f c t =
- let open EConstr in
let rec applyrec (env,(k,c) as acc) t =
(* By using eq_constr, we make an approximation, for instance, we *)
(* could also be interested in finding a term u convertible to t *)
@@ -987,7 +982,7 @@ let apply_on_subterm env evdref f c t =
mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
| _ ->
map_constr_with_binders_left_to_right !evdref
- (fun d (env,(k,c)) -> (push_rel d env, (k+1,Vars.lift 1 c)))
+ (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t
in
applyrec (env,(0,c)) t
@@ -996,7 +991,6 @@ let filter_possible_projections evd c ty ctxt args =
(* Since args in the types will be replaced by holes, we count the
fv of args to have a well-typed filter; don't know how necessary
it is however to have a well-typed filter here *)
- let open EConstr in
let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in
let fv2 = collect_vars evd (mkApp (c,args)) in
let len = Array.length args in
@@ -1039,7 +1033,6 @@ let set_solve_evars f = solve_evars := f
exception TypingFailed of evar_map
let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
- let open EConstr in
try
let evi = Evd.find_undefined evd evk in
let env_evar = evar_filtered_env evi in
@@ -1137,7 +1130,6 @@ let to_pb (pb, env, t1, t2) =
(pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2)
let second_order_matching_with_args ts env evd pbty ev l t =
- let open EConstr in
(*
let evd,ev = evar_absorb_arguments env evd ev l in
let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
@@ -1150,7 +1142,6 @@ let second_order_matching_with_args ts env evd pbty ev l t =
UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
- let open EConstr in
let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index ff40a69381..fa3b9ca0b7 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -10,8 +10,9 @@ open Util
open Pp
open Names
open Term
-open Vars
open Termops
+open EConstr
+open Vars
open Namegen
open Environ
open Evd
@@ -75,7 +76,6 @@ 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
@@ -105,19 +105,19 @@ 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, EConstr.of_constr dom, EConstr.of_constr (subst_var id rng)) in
+ let rng = EConstr.of_constr rng in
+ let prod = mkProd (Name id, EConstr.of_constr dom, 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 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 evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
let evrng = mkEvar (fst (destEvar evd rng), evrngargs) in
evd, mkProd (na, evdom, evrng)
@@ -132,7 +132,6 @@ 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 = EConstr.of_constr (Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi))) in
@@ -147,23 +146,21 @@ 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 (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
+ let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+ let lam = mkLambda (Name id, EConstr.of_constr dom, 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 evd lam in
- let evbodyargs = Array.cons (mkRel 1) (Array.map (Vars.lift 1) args) in
+ let evbodyargs = Array.cons (mkRel 1) (Array.map (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
| 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 evd lam in
@@ -177,8 +174,9 @@ let define_evar_as_sort env evd (ev,args) =
let evi = Evd.find_undefined evd ev in
let s = Type u in
let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in
- let sort = destSort concl in
- let evd' = Evd.define ev (mkSort s) evd in
+ let concl = EConstr.of_constr concl in
+ let sort = destSort evd concl in
+ let evd' = Evd.define ev (Constr.mkSort s) evd in
Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
(* Propagation of constraints through application and abstraction:
@@ -187,7 +185,6 @@ 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 c in
match EConstr.kind evd (EConstr.of_constr t) with
@@ -208,7 +205,7 @@ let split_tycon loc env evd tycon =
evd', (n, mk_tycon dom, mk_tycon rng)
let valcon_of_tycon x = x
-let lift_tycon n = Option.map (EConstr.Vars.lift n)
+let lift_tycon n = Option.map (lift n)
let pr_tycon env = function
None -> str "None"
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b1fc7cbe9a..b7db51d5c5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -6,14 +6,16 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+module CVars = Vars
open Util
open CErrors
open Names
open Term
-open Vars
open Environ
open Termops
open Evd
+open EConstr
+open Vars
open Namegen
open Retyping
open Reductionops
@@ -22,7 +24,6 @@ open Pretype_errors
open Sigma.Notations
let normalize_evar evd ev =
- let open EConstr in
match EConstr.kind evd (mkEvar ev) with
| Evar (evk,args) -> (evk,args)
| _ -> assert false
@@ -50,7 +51,6 @@ let refresh_level evd s =
let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
pbty env evd t =
- let open EConstr in
let evdref = ref evd in
let modified = ref false in
let rec refresh status dir t =
@@ -141,7 +141,6 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
exception IllTypedInstance of env * EConstr.types * EConstr.types
let recheck_applications conv_algo env evdref t =
- let open EConstr in
let rec aux env t =
match EConstr.kind !evdref t with
| App (f, args) ->
@@ -154,7 +153,7 @@ let recheck_applications conv_algo env evdref t =
| Prod (na, dom, codom) ->
(match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
| Success evd -> evdref := evd;
- aux (succ i) (Vars.subst1 args.(i) codom)
+ aux (succ i) (subst1 args.(i) codom)
| UnifFailure (evd, reason) ->
Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
| _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
@@ -221,7 +220,6 @@ let restrict_instance evd evk filter argsv =
open Context.Rel.Declaration
let noccur_evar env evd evk c =
- let open EConstr in
let cache = ref Int.Set.empty (* cache for let-ins *) in
let rec occur_rec check_types (k, env as acc) c =
match EConstr.kind evd c with
@@ -234,10 +232,10 @@ let noccur_evar env evd evk c =
if not (Int.Set.mem (i-k) !cache) then
let decl = Environ.lookup_rel i env in
if check_types then
- (cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr (get_type decl))));
+ (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr (get_type decl))));
(match decl with
| LocalAssum _ -> ()
- | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (Vars.lift i (EConstr.of_constr b)))
+ | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr b)))
| Proj (p,c) -> occur_rec true acc c
| _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env))
(occur_rec check_types) acc c
@@ -270,7 +268,6 @@ let compute_var_aliases sign sigma =
sign Id.Map.empty
let compute_rel_aliases var_aliases rels sigma =
- let open EConstr in
snd (List.fold_right
(fun decl (n,aliases) ->
(n-1,
@@ -288,7 +285,7 @@ let compute_rel_aliases var_aliases rels sigma =
try Int.Map.find (p+n) aliases with Not_found -> [] in
Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
| _ ->
- Int.Map.add n [Vars.lift n (mkCast(t,DEFAULTcast,u))] aliases)
+ Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
| LocalAssum _ -> aliases)
)
rels
@@ -301,10 +298,9 @@ let make_alias_map env sigma =
(var_aliases,rel_aliases)
let lift_aliases n (var_aliases,rel_aliases as aliases) =
- let open EConstr in
if Int.equal n 0 then aliases else
(var_aliases,
- Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (Vars.lift n) l))
+ Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
rel_aliases Int.Map.empty)
let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with
@@ -313,7 +309,6 @@ let get_alias_chain_of sigma aliases x = match EConstr.kind sigma x with
| _ -> []
let normalize_alias_opt sigma aliases x =
- let open EConstr in
match get_alias_chain_of sigma aliases x with
| [] -> None
| a::_ when isRel sigma a || isVar sigma a -> Some a
@@ -326,13 +321,11 @@ let normalize_alias sigma aliases x =
| None -> x
let normalize_alias_var sigma var_aliases id =
- let open EConstr in
destVar sigma (normalize_alias sigma (var_aliases,Int.Map.empty) (mkVar id))
let extend_alias sigma decl (var_aliases,rel_aliases) =
- let open EConstr in
let rel_aliases =
- Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (Vars.lift 1) l))
+ Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
rel_aliases Int.Map.empty in
let rel_aliases =
match decl with
@@ -348,7 +341,7 @@ let extend_alias sigma decl (var_aliases,rel_aliases) =
try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
| _ ->
- Int.Map.add 1 [Vars.lift 1 t] rel_aliases)
+ Int.Map.add 1 [lift 1 t] rel_aliases)
| LocalAssum _ -> rel_aliases in
(var_aliases, rel_aliases)
@@ -358,7 +351,6 @@ let expand_alias_once sigma aliases x =
| l -> Some (List.last l)
let expansions_of_var sigma aliases x =
- let open EConstr in
match get_alias_chain_of sigma aliases x with
| [] -> [x]
| a::_ as l when isRel sigma a || isVar sigma a -> x :: List.rev l
@@ -379,7 +371,6 @@ let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t w
let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma)
let free_vars_and_rels_up_alias_expansion sigma aliases c =
- let open EConstr in
let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
@@ -430,7 +421,7 @@ let rec expand_and_check_vars sigma aliases = function
raise Exit
module Constrhash = Hashtbl.Make
- (struct type t = constr
+ (struct type t = Constr.constr
let equal = Term.eq_constr
let hash = hash_constr
end)
@@ -476,7 +467,6 @@ let remove_instance_local_defs evd evk args =
(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
let find_unification_pattern_args env evd l t =
- let open EConstr in
if List.for_all (fun x -> isRel evd x || isVar evd x) l (* common failure case *) then
let aliases = make_alias_map env evd in
match (try Some (expand_and_check_vars evd aliases l) with Exit -> None) with
@@ -488,7 +478,6 @@ let find_unification_pattern_args env evd l t =
let is_unification_pattern_meta env evd nb m l t =
(* Variables from context and rels > nb are implicitly all there *)
(* so we need to be a rel <= nb *)
- let open EConstr in
if List.for_all (fun x -> isRel evd x && destRel evd x <= nb) l then
match find_unification_pattern_args env evd l t with
| Some _ as x when not (dependent evd (EConstr.mkMeta m) t) -> x
@@ -497,7 +486,6 @@ let is_unification_pattern_meta env evd nb m l t =
None
let is_unification_pattern_evar env evd (evk,args) l t =
- let open EConstr in
if List.for_all (fun x -> isRel evd x || isVar evd x) l
&& noccur_evar env evd evk t
then
@@ -528,14 +516,13 @@ let is_unification_pattern (env,nb) evd f l t =
dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
let solve_pattern_eqn env sigma l c =
- let open EConstr in
let c' = List.fold_right (fun a c ->
- let c' = subst_term sigma (Vars.lift 1 a) (Vars.lift 1 c) in
+ let c' = subst_term sigma (lift 1 a) (lift 1 c) in
match EConstr.kind sigma a with
(* Rem: if [a] links to a let-in, do as if it were an assumption *)
| Rel n ->
let open Context.Rel.Declaration in
- let d = map_constr (lift n) (lookup_rel n env) in
+ let d = map_constr (CVars.lift n) (lookup_rel n env) in
let c' = EConstr.of_constr c' in
mkLambda_or_LetIn d c'
| Var id ->
@@ -604,7 +591,6 @@ 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 (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
@@ -637,7 +623,6 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
exception MorePreciseOccurCheckNeeeded
let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
- let open EConstr in
if Evd.is_defined evd evk1 then
(* Some circularity somewhere (see e.g. #3209) *)
raise MorePreciseOccurCheckNeeeded;
@@ -669,8 +654,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
t_in_sign sign filter inst_in_env in
evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
(push_named_context_val d' sign, Filter.extend 1 filter,
- (mkRel 1)::(List.map (Vars.lift 1) inst_in_env),
- (mkRel 1)::(List.map (Vars.lift 1) inst_in_sign),
+ (mkRel 1)::(List.map (lift 1) inst_in_env),
+ (mkRel 1)::(List.map (lift 1) inst_in_sign),
push_rel d env,evd,id::avoid))
rel_sign
(sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
@@ -707,7 +692,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
List.filter (fun (args',id) ->
(* is_conv is maybe too strong (and source of useless computation) *)
(* (at least expansion of aliases is needed) *)
- Array.for_all2 (fun c1 c2 -> is_conv env evd (EConstr.of_constr c1) (EConstr.of_constr c2)) args args') l in
+ Array.for_all2 (fun c1 c2 -> is_conv env evd c1 (EConstr.of_constr c2)) args args') l in
List.map snd l
with Not_found ->
[]
@@ -765,7 +750,6 @@ let rec assoc_up_to_alias sigma aliases y yc = function
| _ -> if EConstr.eq_constr sigma yc c then id else raise Not_found
let rec find_projectable_vars with_evars aliases sigma y subst =
- let open EConstr in
let yc = normalize_alias sigma aliases y in
let is_projectable idc idcl subst' =
(* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
@@ -829,7 +813,6 @@ let rec find_solution_type evarenv = function
let rec do_projection_effects define_fun env ty evd = function
| ProjectVar -> evd
| ProjectEvar ((evk,argsv),evi,id,p) ->
- let open EConstr in
let evd = Evd.define evk (Constr.mkVar id) evd in
(* TODO: simplify constraints involving evk *)
let evd = do_projection_effects define_fun env ty evd p in
@@ -840,7 +823,7 @@ let rec do_projection_effects define_fun env ty evd = function
one (however, regarding coercions, because t is obtained by
unif, we know that no coercion can be inserted) *)
let subst = make_pure_subst evi argsv in
- let ty' = Vars.replace_vars subst (EConstr.of_constr evi.evar_concl) in
+ let ty' = replace_vars subst (EConstr.of_constr evi.evar_concl) in
if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd
else
evd
@@ -875,14 +858,13 @@ type projectibility_status =
let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
let effects = ref [] in
- let open EConstr in
let rec aux k t =
match EConstr.kind evd t with
| Rel i when i>k0+k -> aux' k (mkRel (i-k))
| Var id -> aux' k t
| _ -> map_with_binders evd succ aux k t
and aux' k t =
- try EConstr.of_constr (project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders)
+ try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
with Not_found ->
match expand_alias_once evd aliases t with
| None -> raise Not_found
@@ -983,7 +965,8 @@ let closure_of_filter evd evk = function
| LocalAssum _ ->
false
| LocalDef (_,c,_) ->
- not (isRel c || isVar c)
+ let c = EConstr.of_constr c in
+ not (isRel evd c || isVar evd c)
in
let newfilter = Filter.map_along test filter (evar_context evi) in
(* Now ensure that restriction is at least what is was originally *)
@@ -1009,7 +992,6 @@ let restrict_hyps evd evk filter candidates =
exception EvarSolvedWhileRestricting of evar_map * EConstr.constr
let do_restrict_hyps evd (evk,args as ev) filter candidates =
- let open EConstr in
let filter,candidates = match filter with
| None -> None,candidates
| Some filter -> restrict_hyps evd evk filter candidates in
@@ -1025,7 +1007,6 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
(* ?e is assumed to have no candidates *)
let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
- let open EConstr in
let rhs = expand_vars_in_term env evd rhs in
let filter =
restrict_upon_filter evd evk
@@ -1162,7 +1143,6 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr
(* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
the common domain of definition *)
let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
- let open EConstr in
(* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
let fvs2 = free_vars_and_rels_up_alias_expansion evd aliases (mkEvar ev2) in
let filter1 = restrict_upon_filter evd evk1
@@ -1210,7 +1190,6 @@ let update_evar_source ev1 ev2 evd =
let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
try
- let open EConstr in
let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in
let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
@@ -1230,7 +1209,6 @@ let preferred_orientation evd evk1 evk2 =
| _ -> true
let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
- let open EConstr in
let aliases = make_alias_map env evd in
if preferred_orientation evd evk1 evk2 then
try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
@@ -1248,6 +1226,7 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
let pbty = if force then None else pbty in
let evi = Evd.find evd evk1 in
+ let downcast evk t evd = downcast evk (EConstr.Unsafe.to_constr t) evd in
let evd =
try
(* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j.
@@ -1289,7 +1268,6 @@ type conv_fun_bool =
* depend on these args). *)
let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
- let open EConstr in
let evdref = ref evd in
if Array.equal (fun c1 c2 -> e_eq_constr_univs evdref (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) ) argsv1 argsv2 then !evdref else
(* Filter and restrict if needed *)
@@ -1350,7 +1328,7 @@ let occur_evar_upto_types sigma n c =
else (
seen := Evar.Set.add sp !seen;
Option.iter occur_rec (existential_opt_value sigma e);
- occur_rec (existential_type sigma e))
+ occur_rec (Evd.existential_type sigma e))
| _ -> Constr.iter occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -1385,7 +1363,6 @@ exception OccurCheckIn of evar_map * EConstr.constr
exception MetaOccurInBodyInternal
let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
- let open EConstr in
let aliases = make_alias_map env evd in
let evdref = ref evd in
let progress = ref false in
@@ -1441,7 +1418,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
| LocalAssum _ -> project_variable (mkRel (i-k))
| LocalDef (_,b,_) ->
try project_variable (mkRel (i-k))
- with NotInvertibleUsingOurAlgorithm _ -> imitate envk (Vars.lift i (EConstr.of_constr b)))
+ with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i (EConstr.of_constr b)))
| Var id ->
(match Environ.lookup_named id env' with
| LocalAssum _ -> project_variable t
@@ -1449,13 +1426,13 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
try project_variable t
with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b))
| LetIn (na,b,u,c) ->
- imitate envk (Vars.subst1 b c)
+ imitate envk (subst1 b c)
| Evar (evk',args' as ev') ->
if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs));
(* Evar/Evar problem (but left evar is virtual) *)
let aliases = lift_aliases k aliases in
(try
- let ev = (evk,Array.map (Vars.lift k) argsv) in
+ let ev = (evk,Array.map (lift k) argsv) in
let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
evdref := evd;
body
@@ -1487,8 +1464,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
progress := true;
match
let c,args = decompose_app_vect !evdref t in
+ let args = Array.map EConstr.of_constr args in
match EConstr.kind !evdref (EConstr.of_constr c) with
- | Construct (cstr,u) when Vars.noccur_between !evdref 1 k t ->
+ | Construct (cstr,u) when noccur_between !evdref 1 k t ->
(* This is common case when inferring the return clause of match *)
(* (currently rudimentary: we do not treat the case of multiple *)
(* possible inversions; we do not treat overlap with a possible *)
@@ -1533,7 +1511,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
| _ -> false
in
is_id_subst filter_ctxt (Array.to_list argsv) &&
- Vars.closed0 evd rhs &&
+ closed0 evd rhs &&
Idset.subset (collect_vars evd rhs) !names
in
let body =
@@ -1659,7 +1637,6 @@ let reconsider_conv_pbs conv_algo evd =
(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
- let open EConstr in
try
let t2 = EConstr.of_constr (whd_betaiota evd t2) in (* includes whd_evar *)
let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d473f41bdf..ffd6e73faa 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -163,7 +163,7 @@ let pattern_of_constr env sigma t =
| Ind (sp,u) -> PRef (canonical_gr (IndRef sp))
| Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
| Proj (p, c) ->
- pattern_of_constr env (EConstr.of_constr (Retyping.expand_projection env sigma p c []))
+ pattern_of_constr env (Retyping.expand_projection env sigma p c [])
| Evar (evk,ctxt as ev) ->
(match snd (Evd.evar_source evk sigma) with
| Evar_kinds.MatchingVar (b,id) ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 510417879e..0e0b807441 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -10,10 +10,11 @@ open CErrors
open Util
open Names
open Term
-open Vars
open Termops
open Univ
open Evd
+open EConstr
+open Vars
open Environ
open Context.Rel.Declaration
@@ -574,7 +575,7 @@ struct
zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
| f, (Cst (cst,_,_,params,_)::s) ->
zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
- | f, (Shift n::s) -> zip (Vars.lift n f, s)
+ | f, (Shift n::s) -> zip (lift n f, s)
| f, (Proj (n,m,p,cst_l)::s) when refold ->
zip (best_state sigma (mkProj (p,f),s) cst_l)
| f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
@@ -585,18 +586,18 @@ struct
end
(** The type of (machine) states (= lambda-bar-calculus' cuts) *)
-type state = EConstr.t * EConstr.t Stack.t
+type state = constr * constr Stack.t
-type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
+type contextual_reduction_function = env -> evar_map -> constr -> Constr.constr
type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> EConstr.t -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
+type local_reduction_function = evar_map -> constr -> Constr.constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (Constr.constr, 'r) Sigma.sigma }
type contextual_stack_reduction_function =
- env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+ env -> evar_map -> constr -> constr * constr list
type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
- evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+ evar_map -> constr -> constr * constr list
type contextual_state_reduction_function =
env -> evar_map -> state -> state
@@ -639,7 +640,7 @@ let local_strong whdfun sigma =
let rec strong_prodspine redfun sigma c =
let x = EConstr.of_constr (redfun sigma c) in
match EConstr.kind sigma x with
- | Prod (na,a,b) -> mkProd (na, EConstr.Unsafe.to_constr a,strong_prodspine redfun sigma b)
+ | Prod (na,a,b) -> EConstr.Unsafe.to_constr (mkProd (na,a,EConstr.of_constr (strong_prodspine redfun sigma b)))
| _ -> EConstr.Unsafe.to_constr x
(*************************************)
@@ -656,7 +657,7 @@ let apply_subst recfun env sigma refold cst_l t stack =
| Some (h,stacktl), Lambda (_,_,c) ->
let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
aux (h::env) cst_l' c stacktl
- | _ -> recfun sigma cst_l (EConstr.Vars.substl env t, stack)
+ | _ -> recfun sigma cst_l (substl env t, stack)
in aux env cst_l t stack
let stacklam recfun env sigma t stack =
@@ -673,8 +674,8 @@ let beta_applist sigma (c,l) =
(* Iota reduction tools *)
type 'a miota_args = {
- mP : EConstr.t; (* the result type *)
- mconstr : EConstr.t; (* the constructor *)
+ mP : constr; (* the result type *)
+ mconstr : constr; (* the constructor *)
mci : case_info; (* special info to re-build pattern *)
mcargs : 'a list; (* the constructor's arguments *)
mlf : 'a array } (* the branch code vector *)
@@ -696,7 +697,6 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
let magicaly_constant_of_fixbody env sigma reference bd = function
| Name.Anonymous -> bd
| Name.Name id ->
- let open EConstr in
try
let (cst_mod,cst_sect,_) = Constant.repr3 reference in
let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
@@ -719,7 +719,6 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
| Not_found -> bd
let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
- let open EConstr in
let nbodies = Array.length bodies in
let make_Fi j =
let ind = nbodies-j-1 in
@@ -733,11 +732,10 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo
| None -> bd
| Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
let closure = List.init nbodies make_Fi in
- Vars.substl closure bodies.(bodynum)
+ substl closure bodies.(bodynum)
(** Similar to the "fix" case below *)
let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
- let open EConstr in
let raw_answer =
let env = if refold then Some env else None in
contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
@@ -749,7 +747,6 @@ let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
[] sigma refold Cst_stack.empty raw_answer sk
let reduce_mind_case sigma mia =
- let open EConstr in
match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
(* let ncargs = (fst mia.mci).(i-1) in*)
@@ -764,7 +761,6 @@ let reduce_mind_case sigma mia =
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
- let open EConstr in
let nbodies = Array.length recindices in
let make_Fi j =
let ind = nbodies-j-1 in
@@ -778,14 +774,13 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
| None -> bd
| Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
let closure = List.init nbodies make_Fi in
- Vars.substl closure bodies.(bodynum)
+ substl closure bodies.(bodynum)
(** First we substitute the Rel bodynum by the fixpoint and then we try to
replace the fixpoint by the best constant from [cst_l]
Other rels are directly substituted by constants "magically found from the
context" in contract_fix *)
let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
- let open EConstr in
let raw_answer =
let env = if refold then None else Some env in
contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
@@ -830,7 +825,6 @@ let _ = Goptions.declare_bool_option {
}
let equal_stacks sigma (x, l) (y, l') =
- let open EConstr in
let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in
let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in
match Stack.equal f_equal eq_fix l l' with
@@ -838,7 +832,6 @@ let equal_stacks sigma (x, l) (y, l') =
| Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2)
let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
- let open EConstr in
let open Context.Named.Declaration in
let rec whrec cst_l (x, stack) =
let () = if !debug_RAKAM then
@@ -859,7 +852,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
match c0 with
| Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
(match lookup_rel n env with
- | LocalDef (_,body,_) -> whrec Cst_stack.empty (EConstr.of_constr (lift n body), stack)
+ | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n (EConstr.of_constr body), stack)
| _ -> fold ())
| Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
(match lookup_named id env with
@@ -977,7 +970,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
let u = if Int.equal napp 1 then f else mkApp (f,lc) in
- if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
+ if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
| _ -> fold ()
else fold ()
| _ -> fold ())
@@ -1054,7 +1047,6 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
(** reduction machine without global env and refold machinery *)
let local_whd_state_gen flags sigma =
- let open EConstr in
let rec whrec (x, stack) =
let c0 = EConstr.kind sigma x in
let s = (EConstr.of_kind c0, stack) in
@@ -1077,7 +1069,7 @@ let local_whd_state_gen flags sigma =
| Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
let u = if Int.equal napp 1 then f else mkApp (f,lc) in
- if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
+ if noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
| _ -> s
else s
| _ -> s)
@@ -1276,7 +1268,7 @@ let f_conv_leq ?l2r ?reds env ?evars x y =
let inj = EConstr.Unsafe.to_constr in
Reduction.conv_leq ?l2r ?reds env ?evars (inj x) (inj y)
-let test_trans_conversion (f: EConstr.t Reduction.extended_conversion_function) reds env sigma x y =
+let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
try
let evars ev = safe_evar_value sigma ev in
let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
@@ -1368,9 +1360,8 @@ let default_plain_instance_ident = Id.of_string "H"
(* Try to replace all metas. Does not replace metas in the metas' values
* Differs from (strong whd_meta). *)
let plain_instance sigma s c =
- let open EConstr in
let rec irec n u = match EConstr.kind sigma u with
- | Meta p -> (try Vars.lift n (Metamap.find p s) with Not_found -> u)
+ | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
| App (f,l) when isCast sigma f ->
let (f,_,t) = destCast sigma f in
let l' = CArray.Fun1.smartmap irec n l in
@@ -1382,13 +1373,13 @@ let plain_instance sigma s c =
(try let g = Metamap.find p s in
match EConstr.kind sigma g with
| App _ ->
- let l' = CArray.Fun1.smartmap Vars.lift 1 l' in
+ let l' = CArray.Fun1.smartmap lift 1 l' in
mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
| _ -> mkApp (g,l')
with Not_found -> mkApp (f,l'))
| _ -> mkApp (irec n f,l'))
| Cast (m,_,_) when isMeta sigma m ->
- (try Vars.lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
+ (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
| _ ->
map_with_binders sigma succ irec n u
in
@@ -1440,9 +1431,8 @@ let instance sigma s c =
* error message. *)
let hnf_prod_app env sigma t n =
- let open EConstr in
match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
- | Prod (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
+ | Prod (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
| _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
let hnf_prod_appvect env sigma t nl =
@@ -1452,9 +1442,8 @@ let hnf_prod_applist env sigma t nl =
List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
let hnf_lam_app env sigma t n =
- let open EConstr in
match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
- | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
+ | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (subst1 n b)
| _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
let hnf_lam_appvect env sigma t nl =
@@ -1544,7 +1533,6 @@ let is_sort env sigma t =
of case/fix (heuristic used by evar_conv) *)
let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
- let open EConstr in
let refold = get_refolding_in_reduction () in
let tactic_mode = false in
let rec whrec csts s =
@@ -1586,7 +1574,6 @@ let is_arity env sigma c =
(* Metas *)
let meta_value evd mv =
- let open EConstr in
let rec valrec mv =
match meta_opt_fvalue evd mv with
| Some (b,_) ->
@@ -1617,54 +1604,58 @@ let meta_reducible_instance evd b =
in
let metas = Metaset.fold fold fm Metamap.empty in
let rec irec u =
- let u = whd_betaiota Evd.empty (EConstr.of_constr u) (** FIXME *) in
- match kind_of_term u with
- | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) ->
- let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in
+ let u = whd_betaiota Evd.empty u (** FIXME *) in
+ let u = EConstr.of_constr u in
+ match EConstr.kind evd u with
+ | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd c)) ->
+ let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd c)) in
(match
try
let g, s = Metamap.find m metas in
+ let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
- if isConstruct g || not is_coerce then Some g else None
+ if isConstruct evd g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkCase (ci,p,g,bl))
| None -> mkCase (ci,irec p,c,Array.map irec bl))
- | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr f))) ->
- let m = destMeta (strip_outer_cast evd (EConstr.of_constr f)) in
+ | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd f)) ->
+ let m = destMeta evd (EConstr.of_constr (strip_outer_cast evd f)) in
(match
try
let g, s = Metamap.find m metas in
+ let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
- if isLambda g || not is_coerce then Some g else None
+ if isLambda evd g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkApp (g,l))
| None -> mkApp (f,Array.map irec l))
| Meta m ->
(try let g, s = Metamap.find m metas in
+ let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if not is_coerce then irec g else u
with Not_found -> u)
- | Proj (p,c) when isMeta c || isCast c && isMeta (pi1 (destCast c)) ->
- let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+ | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) ->
+ let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in
(match
try
let g, s = Metamap.find m metas in
+ let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
- if isConstruct g || not is_coerce then Some g else None
+ if isConstruct evd g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkProj (p,g))
| None -> mkProj (p,c))
- | _ -> Constr.map irec u
+ | _ -> EConstr.map evd irec u
in
if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
- else irec b.rebus
+ else EConstr.Unsafe.to_constr (irec (EConstr.of_constr b.rebus))
let head_unfold_under_prod ts env sigma c =
- let open EConstr in
let unfold (cst,u as cstu) =
if Cpred.mem cst (snd ts) then
match constant_opt_value_in env cstu with
@@ -1682,12 +1673,11 @@ let head_unfold_under_prod ts env sigma c =
EConstr.Unsafe.to_constr (aux c)
let betazetaevar_applist sigma n c l =
- let open EConstr in
let rec stacklam n env t stack =
- if Int.equal n 0 then applist (Vars.substl env t, stack) else
+ if Int.equal n 0 then applist (substl env t, stack) else
match EConstr.kind sigma t, stack with
| Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
- | LetIn(_,b,_,c), _ -> stacklam (n-1) (Vars.substl env b::env) c stack
- | Evar _, _ -> applist (Vars.substl env t, stack)
+ | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
+ | Evar _, _ -> applist (substl env t, stack)
| _ -> anomaly (Pp.str "Not enough lambda/let's") in
EConstr.Unsafe.to_constr (stacklam n [] c l)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a7ccf98a66..6f03fc462a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -10,13 +10,14 @@ open Pp
open CErrors
open Util
open Term
-open Vars
open Inductive
open Inductiveops
open Names
open Reductionops
open Environ
open Termops
+open EConstr
+open Vars
open Arguments_renaming
open Context.Rel.Declaration
@@ -58,7 +59,6 @@ let local_def (na, b, t) =
LocalDef (na, inj b, inj t)
let get_type_from_constraints env sigma t =
- let open EConstr in
if isEvar sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) then
match
List.map_filter (fun (pbty,env,t1,t2) ->
@@ -74,19 +74,17 @@ let get_type_from_constraints env sigma t =
let rec subst_type env sigma typ = function
| [] -> typ
| h::rest ->
- let open EConstr in
match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma typ)) with
- | Prod (na,c1,c2) -> subst_type env sigma (Vars.subst1 h c2) rest
+ | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
| _ -> retype_error NonFunctionalConstruction
(* If ft is the type of f which itself is applied to args, *)
(* [sort_of_atomic_type] computes ft[args] which has to be a sort *)
let sort_of_atomic_type env sigma ft args =
- let open EConstr in
let rec concl_of_arity env n ar args =
match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma ar)), args with
- | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, Vars.lift n h, t)) env) (n + 1) b l
+ | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, lift n h, t)) env) (n + 1) b l
| Sort s, [] -> s
| _ -> retype_error NotASort
in concl_of_arity env 0 ft (Array.to_list args)
@@ -101,7 +99,6 @@ let decomp_sort env sigma t =
| _ -> retype_error NotASort
let retype ?(polyprop=true) sigma =
- let open EConstr in
let rec type_of env cstr =
match EConstr.kind sigma cstr with
| Meta n ->
@@ -109,7 +106,7 @@ let retype ?(polyprop=true) sigma =
with Not_found -> retype_error (BadMeta n))
| Rel n ->
let ty = EConstr.of_constr (RelDecl.get_type (lookup_rel n env)) in
- Vars.lift n ty
+ lift n ty
| Var id -> type_of_var env id
| Const cst -> EConstr.of_constr (rename_type_of_constant env cst)
| Evar (evk, args) -> EConstr.of_constr (Evd.existential_type sigma (evk, Array.map EConstr.Unsafe.to_constr args))
@@ -133,7 +130,7 @@ let retype ?(polyprop=true) sigma =
| Lambda (name,c1,c2) ->
mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2)
| LetIn (name,b,c1,c2) ->
- Vars.subst1 b (type_of (push_rel (local_def (name,b,c1)) env) c2)
+ subst1 b (type_of (push_rel (local_def (name,b,c1)) env) c2)
| Fix ((_,i),(_,tys,_)) -> tys.(i)
| CoFix (i,(_,tys,_)) -> tys.(i)
| App(f,args) when is_template_polymorphic env sigma f ->
@@ -257,11 +254,11 @@ let sorts_of_context env evc ctxt =
snd (aux ctxt)
let expand_projection env sigma pr c args =
- let inj = EConstr.Unsafe.to_constr in
let ty = get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
with Not_found -> retype_error BadRecursiveType
in
+ let ind_args = List.map EConstr.of_constr ind_args in
mkApp (mkConstU (Projection.constant pr,u),
- Array.of_list (ind_args @ (inj c :: List.map inj args)))
+ Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index c844038904..a20b11b76e 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -45,6 +45,6 @@ val type_of_global_reference_knowing_conclusion :
val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
-val expand_projection : env -> evar_map -> Names.projection -> EConstr.constr -> EConstr.constr list -> constr
+val expand_projection : env -> evar_map -> Names.projection -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val print_retype_error : retype_error -> Pp.std_ppcmds
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5b8eaa50b1..ae53c12ae7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -11,10 +11,11 @@ open CErrors
open Util
open Names
open Term
-open Vars
open Libnames
open Globnames
open Termops
+open EConstr
+open Vars
open Find_subterm
open Namegen
open Environ
@@ -88,7 +89,6 @@ let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
| _ -> false
let mkEvalRef ref u =
- let open EConstr in
match ref with
| EvalConst cst -> mkConstU (cst,u)
| EvalVar id -> mkVar id
@@ -109,7 +109,6 @@ let destEvalRefU sigma c = match EConstr.kind sigma c with
| _ -> anomaly (Pp.str "Not an unfoldable reference")
let unsafe_reference_opt_value env sigma eval =
- let open EConstr in
match eval with
| EvalConst cst ->
(match (lookup_constant cst env).Declarations.const_body with
@@ -118,20 +117,19 @@ let unsafe_reference_opt_value env sigma eval =
| EvalVar id ->
env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
| EvalRel n ->
- env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value |> Option.map EConstr.of_constr
+ env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n)
| EvalEvar ev ->
match EConstr.kind sigma (mkEvar ev) with
| Evar _ -> None
| c -> Some (EConstr.of_kind c)
let reference_opt_value env sigma eval u =
- let open EConstr in
match eval with
| EvalConst cst -> Option.map EConstr.of_constr (constant_opt_value_in env (cst,u))
| EvalVar id ->
env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
| EvalRel n ->
- env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value |> Option.map EConstr.of_constr
+ env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n)
| EvalEvar ev ->
match EConstr.kind sigma (mkEvar ev) with
| Evar _ -> None
@@ -187,7 +185,6 @@ let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation"
*)
let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
- let open EConstr in
let n = List.length labs in
let nargs = List.length args in
if nargs > n then raise Elimconst;
@@ -232,7 +229,6 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
let invert_name labs l na0 env sigma ref = function
| Name id ->
- let open EConstr in
let minfxargs = List.length l in
begin match na0 with
| Name id' when Id.equal id' id ->
@@ -276,7 +272,6 @@ let local_def (na, b, t) =
LocalDef (na, inj b, inj t)
let compute_consteval_direct env sigma ref =
- let open EConstr in
let rec srec env n labs onlyproj c =
let c',l = whd_betadeltazeta_stack env sigma c in
match EConstr.kind sigma c' with
@@ -295,7 +290,6 @@ let compute_consteval_direct env sigma ref =
| Some c -> srec env 0 [] false c
let compute_consteval_mutual_fix env sigma ref =
- let open EConstr in
let rec srec env minarg labs ref c =
let c',l = whd_betalet_stack sigma c in
let nargs = List.length l in
@@ -367,7 +361,6 @@ let reference_eval env sigma = function
let x = Name default_dependent_ident
let make_elim_fun (names,(nbfix,lv,n)) u largs =
- let open EConstr in
let lu = List.firstn n largs in
let p = List.length lv in
let lyi = List.map fst lv in
@@ -393,7 +386,7 @@ let make_elim_fun (names,(nbfix,lv,n)) u largs =
(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]:
do so that the reduction uses this extra information *)
-let dummy = mkProp
+let dummy = Constr.mkProp
let vfx = Id.of_string "_expanded_fix_"
let vfun = Id.of_string "_eliminator_function_"
let venv = let open Context.Named.Declaration in
@@ -403,7 +396,6 @@ let venv = let open Context.Named.Declaration in
as a problem variable: an evar that can be instantiated either by
vfx (expanded fixpoint) or vfun (named function). *)
let substl_with_function subst sigma constr =
- let open EConstr in
let evd = ref sigma in
let minargs = ref Evar.Map.empty in
let v = Array.of_list subst in
@@ -431,8 +423,7 @@ exception Partial
reduction is solved by the expanded fix term. *)
let solve_arity_problem env sigma fxminargs c =
let evm = ref sigma in
- let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
- let open EConstr in
+ let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in
let rec check strict c =
let c' = EConstr.of_constr (whd_betaiotazeta sigma c) in
let (h,rcargs) = decompose_app_vect sigma c' in
@@ -491,7 +482,6 @@ let reduce_fix whdfun sigma fix stack =
let contract_fix_use_function env sigma f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
- let open EConstr in
let nbodies = Array.length recindices in
let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
let lbodies = List.init nbodies make_Fi in
@@ -515,7 +505,6 @@ let reduce_fix_use_function env sigma f whfun fix stack =
let contract_cofix_use_function env sigma f
(bodynum,(_names,_,bodies as typedbodies)) =
- let open EConstr in
let nbodies = Array.length bodies in
let make_Fi j = (mkCoFix(j,typedbodies), f j) in
let subbodies = List.init nbodies make_Fi in
@@ -523,7 +512,6 @@ let contract_cofix_use_function env sigma f
sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
let reduce_mind_case_use_function func env sigma mia =
- let open EConstr in
match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
@@ -573,11 +561,10 @@ let match_eval_ref_value env sigma constr =
| Var id when is_evaluable env (EvalVarRef id) ->
env |> lookup_named id |> NamedDecl.get_value |> Option.map EConstr.of_constr
| Rel n ->
- env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value |> Option.map EConstr.of_constr
+ env |> lookup_rel n |> RelDecl.get_value |> Option.map (EConstr.of_constr %> lift n)
| _ -> None
let special_red_case env sigma whfun (ci, p, c, lf) =
- let open EConstr in
let rec redrec s =
let (constr, cargs) = whfun s in
match match_eval_ref env sigma constr with
@@ -614,7 +601,6 @@ let reduce_projection env sigma pb (recarg'hd,stack') stack =
| _ -> NotReducible)
let reduce_proj env sigma whfun whfun' c =
- let open EConstr in
let rec redrec s =
match EConstr.kind sigma s with
| Proj (proj, c) ->
@@ -641,7 +627,7 @@ let whd_nothing_for_iota env sigma s =
| Rel n ->
let open Context.Rel.Declaration in
(match lookup_rel n env with
- | LocalDef (_,body,_) -> whrec (EConstr.of_constr (lift n body), stack)
+ | LocalDef (_,body,_) -> whrec (lift n (EConstr.of_constr body), stack)
| _ -> s)
| Var id ->
let open Context.Named.Declaration in
@@ -673,7 +659,6 @@ let whd_nothing_for_iota env sigma s =
it fails if no redex is around *)
let rec red_elim_const env sigma ref u largs =
- let open EConstr in
let nargs = List.length largs in
let largs, unfold_anyway, unfold_nonelim, nocase =
match recargs ref with
@@ -747,7 +732,6 @@ and reduce_params env sigma stack l =
a reducible iota/fix/cofix redex (the "simpl" tactic) *)
and whd_simpl_stack env sigma =
- let open EConstr in
let rec redrec s =
let (x, stack) = decompose_app_vect sigma s in
let stack = Array.map_to_list EConstr.of_constr stack in
@@ -818,7 +802,6 @@ and whd_simpl_stack env sigma =
(* reduce until finding an applied constructor or fail *)
and whd_construct_stack env sigma s =
- let open EConstr in
let (constr, cargs as s') = whd_simpl_stack env sigma s in
if reducible_mind_case sigma constr then s'
else match match_eval_ref env sigma constr with
@@ -838,7 +821,6 @@ and whd_construct_stack env sigma s =
let try_red_product env sigma c =
let simpfun c = EConstr.of_constr (clos_norm_flags betaiotazeta env sigma c) in
- let open EConstr in
let rec redrec env x =
let x = EConstr.of_constr (whd_betaiota sigma x) in
match EConstr.kind sigma x with
@@ -948,7 +930,6 @@ let whd_simpl_stack =
immediately hides a non reducible fix or a cofix *)
let whd_simpl_orelse_delta_but_fix env sigma c =
- let open EConstr in
let rec redrec s =
let (constr, stack as s') = whd_simpl_stack env sigma s in
match match_eval_ref_value env sigma constr with
@@ -982,7 +963,6 @@ let simpl env sigma c = strong whd_simpl env sigma c
(* Reduction at specific subterms *)
let matches_head env sigma c t =
- let open EConstr in
match EConstr.kind sigma t with
| App (f,_) -> Constr_matching.matches env sigma c f
| Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, Univ.Instance.empty))
@@ -993,11 +973,9 @@ let matches_head env sigma c t =
of the projection and its eta expanded form.
*)
let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
- let open EConstr in
match EConstr.kind sigma c with
| Proj (p, r) -> (* Treat specially for partial applications *)
let t = Retyping.expand_projection env sigma p r [] in
- let t = EConstr.of_constr t in
let hdf, al = destApp sigma t in
let a = al.(Array.length al - 1) in
let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in
@@ -1011,7 +989,6 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
| _ -> map_constr_with_binders_left_to_right sigma g f acc c
let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
- let open EConstr in
let (nowhere_except_in,locs) = Locusops.convert_occs occs in
let maxocc = List.fold_right max locs 0 in
let pos = ref 1 in
@@ -1138,7 +1115,6 @@ let unfoldn loccname env sigma c =
(* Re-folding constants tactics: refold com in term c *)
let fold_one_com com env sigma c =
- let open EConstr in
let rcom =
try EConstr.of_constr (red_product env sigma com)
with Redelimination -> error "Not reducible." in
@@ -1176,7 +1152,6 @@ let compute = cbv_betadeltaiota
* the specified occurrences. *)
let abstract_scheme env sigma (locc,a) (c, sigma) =
- let open EConstr in
let ta = Retyping.get_type_of env sigma a in
let ta = EConstr.of_constr ta in
let na = named_hd env (EConstr.to_constr sigma ta) Anonymous in
@@ -1189,7 +1164,6 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
mkLambda (na,ta,c'), sigma'
let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
- let open EConstr in
let sigma = Sigma.to_evar_map sigma in
let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
try
@@ -1218,7 +1192,6 @@ let check_not_primitive_record env ind =
return name, B and t' *)
let reduce_to_ind_gen allow_product env sigma t =
- let open EConstr in
let rec elimrec env t l =
let t = hnf_constr env sigma t in
let t = EConstr.of_constr t in
@@ -1246,7 +1219,7 @@ let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma (EConst
let find_hnf_rectype env sigma t =
let ind,t = reduce_to_atomic_ind env sigma t in
- ind, snd (decompose_app t)
+ ind, snd (Term.decompose_app t)
(* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta]
or raise [NotStepReducible] if not a weak-head redex *)
@@ -1254,7 +1227,6 @@ let find_hnf_rectype env sigma t =
exception NotStepReducible
let one_step_reduce env sigma c =
- let open EConstr in
let rec redrec (x, stack) =
match EConstr.kind sigma x with
| Lambda (n,t,c) ->
@@ -1302,7 +1274,6 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
(* lazily reduces to match the head of [t] with the expected [ref] *)
let rec elimrec env t l =
- let open EConstr in
let c, _ = decompose_app_vect sigma t in
let c = EConstr.of_constr c in
match EConstr.kind sigma c with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 17adea5f2c..cf58a0b668 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -65,7 +65,6 @@ let e_assumption_of_judgment env evdref j =
error_assumption env !evdref 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);
@@ -100,7 +99,6 @@ let max_sort l =
if Sorts.List.mem InSet l then InSet else InProp
let e_is_correct_arity env evdref c pj ind specif params =
- let open EConstr in
let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
let allowed_sorts = elim_sorts specif in
let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
@@ -124,7 +122,6 @@ let e_is_correct_arity env evdref c pj ind specif params =
srec env pj.uj_type (List.rev arsign)
let lambda_applist_assum sigma n c l =
- let open EConstr in
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
@@ -150,7 +147,6 @@ let e_type_case_branches env evdref (ind,largs) pj c =
(lc, ty)
let e_judge_of_case env evdref ci pj cj lfj =
- let open EConstr in
let indspec =
try find_mrectype env !evdref cj.uj_type
with Not_found -> error_case_not_inductive env !evdref cj in
@@ -161,7 +157,6 @@ let e_judge_of_case env evdref ci pj cj lfj =
uj_type = rslty }
let check_type_fixpoint loc env evdref lna lar vdefj =
- let open EConstr in
let lt = Array.length vdefj in
if Int.equal (Array.length lar) lt then
for i = 0 to lt-1 do
@@ -183,7 +178,6 @@ let check_allowed_sort env sigma ind c p =
(Some(ksort,s,Type_errors.error_elim_explain ksort s))
let e_judge_of_cast env evdref cj k tj =
- let open EConstr in
let expected_type = tj.utj_val in
if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
error_actual_type_core env !evdref cj expected_type;
@@ -259,7 +253,6 @@ let judge_of_letin env name defj typj j =
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
let rec execute env evdref cstr =
- let open EConstr in
let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
match EConstr.kind !evdref cstr with
| Meta n ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1b209fa772..483fefaf2e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -85,7 +85,6 @@ let occur_meta_evd sigma mv c =
gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
let abstract_scheme env evd c l lname_typ =
- let open EConstr in
let mkLambda_name env (n,a,b) =
mkLambda (named_hd env (EConstr.Unsafe.to_constr a) n, a, b)
in
@@ -131,7 +130,6 @@ 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
@@ -195,8 +193,6 @@ let pose_all_metas_as_evars env evd t =
(!evdref, c)
let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0) =
- let open EConstr in
- let open Vars in
match EConstr.kind sigma f with
| Meta k ->
(* We enforce that the Meta does not depend on the [nb]
@@ -476,7 +472,6 @@ let use_evars_pattern_unification flags =
&& Flags.version_strictly_greater Flags.V8_2
let use_metas_pattern_unification sigma flags nb l =
- let open EConstr in
!global_pattern_unification_flag && flags.use_pattern_unification
|| (Flags.version_less_or_equal Flags.V8_3 ||
flags.use_meta_bound_pattern_unification) &&
@@ -636,7 +631,6 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM
let rec is_neutral env sigma ts t =
- let open EConstr in
let (f, l) = decompose_app_vect sigma t in
match EConstr.kind sigma (EConstr.of_constr f) with
| Const (c, u) ->
@@ -666,7 +660,6 @@ let is_eta_constructor_app env sigma ts f l1 term =
| _ -> false
let eta_constructor_app env sigma f l1 term =
- let open EConstr in
match EConstr.kind sigma f with
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
@@ -684,8 +677,6 @@ let print_constr_env env c =
print_constr_env env (EConstr.Unsafe.to_constr c)
let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n =
- let open EConstr in
- let open Vars in
let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn =
let cM = Evarutil.whd_head_evar sigma curm
and cN = Evarutil.whd_head_evar sigma curn in
@@ -892,7 +883,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let expand_proj c c' l =
match EConstr.kind sigma c with
| Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' ->
- (try destApp sigma (EConstr.of_constr (Retyping.expand_projection curenv sigma p t (Array.to_list l)))
+ (try destApp sigma (Retyping.expand_projection curenv sigma p t (Array.to_list l))
with RetypeError _ -> (** Unification can be called on ill-typed terms, due
to FO and eta in particular, fail gracefully in that case *)
(c, l))
@@ -1128,8 +1119,6 @@ let right = false
let rec unify_with_eta keptside flags env sigma c1 c2 =
(* Question: try whd_all on ci if not two lambdas? *)
- let open EConstr in
- let open Vars in
match EConstr.kind sigma c1, EConstr.kind sigma c2 with
| (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
let env' = push_rel_assum (na,t1) env in
@@ -1234,8 +1223,6 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
* since other metavars might also need to be resolved. *)
let applyHead env (type r) (evd : r Sigma.t) n c =
- let open EConstr in
- let open Vars in
let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma =
fun n c cty p evd ->
if Int.equal n 0 then
@@ -1307,7 +1294,6 @@ let order_metas metas =
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
let solve_simple_evar_eqn ts env evd ev rhs =
- let open EConstr in
match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
| UnifFailure (evd,reason) ->
error_cannot_unify env evd ~reason (mkEvar ev,rhs);
@@ -1319,8 +1305,6 @@ let solve_simple_evar_eqn ts env evd ev rhs =
is true, unification of types of metas is required *)
let w_merge env with_types flags (evd,metas,evars : subst0) =
- let open EConstr in
- let open Vars in
let rec w_merge_rec evd metas evars eqns =
(* Process evars *)
@@ -1498,7 +1482,6 @@ let w_unify_core_0 env evd with_types cv_pb flags m n =
let w_typed_unify env evd = w_unify_core_0 env evd true
let w_typed_unify_array env evd flags f1 l1 f2 l2 =
- let open EConstr in
let f1 = EConstr.of_constr f1 in
let f2 = EConstr.of_constr f2 in
let l1 = Array.map EConstr.of_constr l1 in
@@ -1529,7 +1512,6 @@ let iter_fail f a =
contexts, with evars, and possibly with occurrences *)
let indirectly_dependent sigma c d decls =
- let open EConstr in
not (isVar sigma c) &&
(* This test is not needed if the original term is a variable, but
it is needed otherwise, as e.g. when abstracting over "2" in
@@ -1590,7 +1572,6 @@ let default_matching_flags (sigma,_) =
exception PatternNotFound
let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
- let open EConstr in
let flags =
if from_prefix_of_ind then
let flags = default_matching_flags pending in
@@ -1600,7 +1581,6 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
else default_matching_flags pending in
let n = Array.length (snd (decompose_app_vect sigma c)) in
let matching_fun _ t =
- let open EConstr in
try
let t',l2 =
if from_prefix_of_ind then
@@ -1754,8 +1734,6 @@ let keyed_unify env evd kop =
Unifies [cl] to every subterm of [op] until it finds a match.
Fails if no match is found *)
let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
- let open EConstr in
- let open Vars in
let bestexn = ref None in
let kop = Keys.constr_key (EConstr.to_constr evd op) in
let rec matchrec cl =
@@ -1831,8 +1809,6 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
Unifies [cl] to every subterm of [op] and return all the matches.
Fails if no match is found *)
let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
- let open EConstr in
- let open Vars in
let return a b =
let (evd,c as a) = a () in
if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b
@@ -1897,7 +1873,6 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
| _ -> res
let w_unify_to_subterm_list env evd flags hdmeta oplist t =
- let open EConstr in
List.fold_right
(fun op (evd,l) ->
let op = whd_meta evd op in
@@ -2008,7 +1983,6 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
- let open EConstr in
let hd1,l1 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty1)) in
let hd2,l2 = decompose_app_vect evd (EConstr.of_constr (whd_nored evd ty2)) in
let is_empty1 = Array.is_empty l1 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2cb9e08648..eebb2a0380 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3165,7 +3165,7 @@ let expand_projections env sigma c =
let sigma = Sigma.to_evar_map sigma in
let rec aux env c =
match EConstr.kind sigma c with
- | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (aux env c) [])
+ | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
| _ -> map_constr_with_full_binders sigma push_rel aux env c
in
EConstr.Unsafe.to_constr (aux env (EConstr.of_constr c))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:52:17 +0000