aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml9
-rw-r--r--pretyping/classops.ml1
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evardefine.ml17
-rw-r--r--pretyping/evarsolve.ml13
-rw-r--r--pretyping/inductiveops.ml1
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/tacred.ml8
-rw-r--r--pretyping/tacred.mli10
-rw-r--r--pretyping/unification.ml9
13 files changed, 44 insertions, 44 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 57d12a19f6..360199fecb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -297,7 +297,7 @@ let inductive_template evdref env tmloc ind =
| LocalAssum (na,ty) ->
let ty = EConstr.of_constr ty in
let ty' = substl subst ty in
- let e = EConstr.of_constr (e_new_evar env evdref ~src:(hole_source n) ty') in
+ let e = e_new_evar env evdref ~src:(hole_source n) ty' in
(e::subst,e::evarl,n+1)
| LocalDef (na,b,ty) ->
let b = EConstr.of_constr b in
@@ -380,7 +380,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl =
(* Utils *)
let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref =
- let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in EConstr.of_constr e
+ let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
let evd_comb2 f evdref x y =
let (evd',y) = f !evdref x y in
@@ -1663,7 +1663,6 @@ let abstract_tycon loc env evdref subst tycon extenv t =
1 (rel_context env) in
let ty = EConstr.of_constr ty in
let ev' = e_new_evar env evdref ~src ty in
- let ev' = EConstr.of_constr ev' in
begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
@@ -1698,7 +1697,6 @@ let abstract_tycon loc env evdref subst tycon extenv t =
let candidates = u :: List.map mkRel vl in
let candidates = List.map EConstr.Unsafe.to_constr candidates in
let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
- let ev = EConstr.of_constr ev in
lift k ev
in
aux (0,extenv,subst0) t0
@@ -1712,7 +1710,6 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
let n' = Context.Rel.length (rel_context tycon_env) in
let impossible_case_type, u =
e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in
- let impossible_case_type = EConstr.of_constr impossible_case_type in
(lift (n'-n) impossible_case_type, mkSort u)
| Some t ->
let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
@@ -2010,7 +2007,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let Sigma ((t, _), sigma, _) =
new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
let sigma = Sigma.to_evar_map sigma in
- sigma, EConstr.of_constr t
+ sigma, t
in
(* First strategy: we build an "inversion" predicate *)
let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9011186a3d..23d20dad3e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -51,6 +51,7 @@ type coe_info_typ = {
coe_param : int }
let coe_info_typ_equal c1 c2 =
+ let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in
eq_constr c1.coe_value c2.coe_value &&
eq_constr c1.coe_type c2.coe_type &&
c1.coe_local == c2.coe_local &&
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e7279df7a5..d67976232a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -93,7 +93,7 @@ open Program
let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c =
let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
- EConstr.of_constr (Evarutil.e_new_evar env evdref ~src c)
+ Evarutil.e_new_evar env evdref ~src c
let app_opt env evdref f t =
EConstr.of_constr (whd_betaiota !evdref (app_opt f t))
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 4756ec30e7..ec8945e85e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -294,7 +294,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
| na::nal ->
match kind_of_term c with
| Case (ci,p,c,cl) when
- eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
+ eq_constr sigma (EConstr.of_constr c) (EConstr.mkRel (List.index Name.equal na (fst (snd e))))
&& not (Int.equal (Array.length cl) 0)
&& (* don't contract if p dependent *)
computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ee6355736b..a968af7ff2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -890,7 +890,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
let i = Sigma.Unsafe.of_evar_map i 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))
+ (i', ev :: ks, m - 1,test))
(evd,[],List.length bs,fun i -> Success i) bs
in
let app = mkApp (c, Array.rev_of_list ks) in
@@ -1066,13 +1066,13 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| Some _ -> error "Selection of specific occurrences not supported"
| None ->
let evty = set_holes evdref cty subst in
- let instance = List.map EConstr.Unsafe.to_constr (Filter.filter_list filter instance) in
+ let instance = Filter.filter_list filter instance in
let evd = Sigma.Unsafe.of_evar_map !evdref in
let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
let evd = Sigma.to_evar_map evd in
evdref := evd;
- evsref := (fst (destEvar !evdref (EConstr.of_constr ev)),evty)::!evsref;
- EConstr.of_constr ev in
+ evsref := (fst (destEvar !evdref ev),evty)::!evsref;
+ ev in
set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
| [] -> rhs in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index fa3b9ca0b7..3babc48a7f 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -22,6 +22,11 @@ open Sigma.Notations
module RelDecl = Context.Rel.Declaration
+let nlocal_assum (na, t) =
+ let open Context.Named.Declaration in
+ let inj = EConstr.Unsafe.to_constr in
+ LocalAssum (na, inj t)
+
let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
let evd = Sigma.Unsafe.of_evar_map evd in
let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
@@ -88,7 +93,7 @@ let define_pure_evar_as_product evd evk =
(Sigma.to_evar_map evd1, e)
in
let evd2,rng =
- let newenv = push_named (LocalAssum (id, dom)) evenv in
+ let newenv = push_named (nlocal_assum (id, dom)) evenv in
let src = evar_source evk evd1 in
let filter = Filter.extend 1 (evar_filter evi) in
if is_prop_sort s then
@@ -105,8 +110,7 @@ let define_pure_evar_as_product evd evk =
let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
evd3, rng
in
- let rng = EConstr.of_constr rng in
- let prod = mkProd (Name id, EConstr.of_constr dom, subst_var id rng) in
+ let prod = mkProd (Name id, dom, subst_var id rng) in
let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in
evd3,prod
@@ -140,14 +144,13 @@ let define_pure_evar_as_lambda env evd evk =
| Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
| _ -> error_not_product env evd typ in
let avoid = ids_of_named_context (evar_context evi) in
- let dom = EConstr.Unsafe.to_constr dom in
let id =
- next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
- let newenv = push_named (LocalAssum (id, dom)) evenv in
+ next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd (EConstr.Unsafe.to_constr dom)) in
+ let newenv = push_named (nlocal_assum (id, dom)) evenv in
let filter = Filter.extend 1 (evar_filter evi) in
let src = evar_source evk evd1 in
let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
- let lam = mkLambda (Name id, EConstr.of_constr dom, subst_var id (EConstr.of_constr body)) in
+ let lam = mkLambda (Name id, dom, subst_var id body) in
Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
let define_evar_as_lambda env evd (evk,args) =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b7db51d5c5..4ce8a44adc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -518,15 +518,15 @@ let is_unification_pattern (env,nb) evd f l t =
let solve_pattern_eqn env sigma l c =
let c' = List.fold_right (fun a c ->
let c' = subst_term sigma (lift 1 a) (lift 1 c) in
+ let c' = EConstr.of_constr 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 (CVars.lift n) (lookup_rel n env) in
- let c' = EConstr.of_constr c' in
mkLambda_or_LetIn d c'
| Var id ->
- let d = lookup_named id env in EConstr.of_constr (mkNamedLambda_or_LetIn d c')
+ let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
| _ -> assert false)
l c in
(* Warning: we may miss some opportunity to eta-reduce more since c'
@@ -592,10 +592,9 @@ 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 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 Sigma (evar_in_env, evd, _) = new_evar_instance sign evd (EConstr.of_constr ty_t_in_sign) ~filter ~src inst_in_env in
let evd = Sigma.to_evar_map evd in
let t_in_env = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr t_in_env)) in
- let evar_in_env = EConstr.of_constr evar_in_env in
let (evk, _) = destEvar evd evar_in_env in
let evd = define_fun env evd None (EConstr.destEvar evd evar_in_env) t_in_env in
let ctxt = named_context_of_val sign in
@@ -669,10 +668,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let evd = Sigma.Unsafe.of_evar_map evd in
let ev2ty_in_sign = EConstr.of_constr ev2ty_in_sign in
let Sigma (ev2_in_sign, evd, _) =
- new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src (List.map EConstr.Unsafe.to_constr inst2_in_sign) in
+ new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
let evd = Sigma.to_evar_map evd in
- let ev2_in_env = (fst (destEvar evd (EConstr.of_constr ev2_in_sign)), Array.of_list inst2_in_env) in
- (evd, EConstr.of_constr ev2_in_sign, ev2_in_env)
+ let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in
+ (evd, ev2_in_sign, ev2_in_env)
let restrict_upon_filter evd evk p args =
let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e30ba21fd1..98b267cfd4 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -556,6 +556,7 @@ let set_pattern_names env ind brv =
let type_case_branches_with_names env sigma indspec p c =
let (ind,args) = indspec in
+ let args = List.map EConstr.Unsafe.to_constr args in
let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
let (params,realargs) = List.chop nparams args in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cf5523a50d..7af9731f9a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -175,7 +175,7 @@ val arity_of_case_predicate :
env -> inductive_family -> bool -> sorts -> types
val type_case_branches_with_names :
- env -> evar_map -> pinductive * constr list -> constr -> constr -> types array * types
+ env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types
(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 49a0bccee9..7586b54ba1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -116,7 +116,7 @@ let lookup_named id env = lookup_named id env.env
let e_new_evar env evdref ?src ?naming typ =
let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
let open Context.Named.Declaration in
- let inst_vars = List.map (get_id %> Constr.mkVar) (named_context env.env) in
+ let inst_vars = List.map (get_id %> EConstr.mkVar) (named_context env.env) in
let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
let (subst, vsubst, _, nc) = Lazy.force env.extra in
let typ' = subst2 subst vsubst typ in
@@ -125,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ =
let sigma = Sigma.Unsafe.of_evar_map !evdref in
let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in
evdref := Sigma.to_evar_map sigma;
- EConstr.of_constr e
+ e
let push_rec_types (lna,typarray,_) env =
let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in
@@ -546,7 +546,7 @@ let new_type_evar env evdref loc =
univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
in
evdref := Sigma.to_evar_map sigma;
- EConstr.of_constr e
+ e
let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 24d4af89a6..1ec8deb1b5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1196,7 +1196,7 @@ let reduce_to_ind_gen allow_product env sigma t =
let t = hnf_constr env sigma t in
let t = EConstr.of_constr t in
match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) with
- | Ind ind-> (check_privacy env ind, EConstr.Unsafe.to_constr (it_mkProd_or_LetIn t l))
+ | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
| Prod (n,ty,t') ->
let open Context.Rel.Declaration in
if allow_product then
@@ -1209,7 +1209,7 @@ let reduce_to_ind_gen allow_product env sigma t =
let t' = whd_all env sigma t in
let t' = EConstr.of_constr t' in
match EConstr.kind sigma (EConstr.of_constr (fst (decompose_app_vect sigma t'))) with
- | Ind ind-> (check_privacy env ind, EConstr.Unsafe.to_constr (it_mkProd_or_LetIn t' l))
+ | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
| _ -> user_err (str"Not an inductive product.")
in
elimrec env t []
@@ -1219,7 +1219,7 @@ let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma c
let find_hnf_rectype env sigma t =
let ind,t = reduce_to_atomic_ind env sigma t in
- ind, snd (Term.decompose_app t)
+ ind, snd (decompose_app sigma t)
(* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta]
or raise [NotStepReducible] if not a weak-head redex *)
@@ -1295,7 +1295,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
elimrec env t' l
with NotStepReducible -> error_cannot_recognize ref
in
- EConstr.Unsafe.to_constr (elimrec env t [])
+ elimrec env t []
let reduce_to_quantified_ref = reduce_to_ref_gen true
let reduce_to_atomic_ref = reduce_to_ref_gen false
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 3587ae2810..15b4e990d8 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -75,23 +75,23 @@ val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function
(** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
with [I] an inductive definition;
returns [I] and [t'] or fails with a user error *)
-val reduce_to_atomic_ind : env -> evar_map -> EConstr.types -> pinductive * types
+val reduce_to_atomic_ind : env -> evar_map -> EConstr.types -> pinductive * EConstr.types
(** [reduce_to_quantified_ind env sigma t] puts [t] in the form
[t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
returns [I] and [t'] or fails with a user error *)
-val reduce_to_quantified_ind : env -> evar_map -> EConstr.types -> pinductive * types
+val reduce_to_quantified_ind : env -> evar_map -> EConstr.types -> pinductive * EConstr.types
(** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
[t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
val reduce_to_quantified_ref :
- env -> evar_map -> global_reference -> EConstr.types -> types
+ env -> evar_map -> global_reference -> EConstr.types -> EConstr.types
val reduce_to_atomic_ref :
- env -> evar_map -> global_reference -> EConstr.types -> types
+ env -> evar_map -> global_reference -> EConstr.types -> EConstr.types
val find_hnf_rectype :
- env -> evar_map -> EConstr.types -> pinductive * constr list
+ env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list
val contextually : bool -> occurrences * constr_pattern ->
(patvar_map -> reduction_function) -> reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2b2069ec45..bc59a41087 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -133,14 +133,14 @@ let abstract_list_all_with_dependencies env evd typ c l =
let evd = Sigma.Unsafe.of_evar_map evd in
let Sigma (ev, evd, _) = new_evar env evd typ in
let evd = Sigma.to_evar_map evd in
- let evd,ev' = evar_absorb_arguments env evd (destEvar evd (EConstr.of_constr ev)) l in
+ let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in
let n = List.length l in
let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
let evd,b =
Evarconv.second_order_matching empty_transparent_state
env evd ev' argoccs c in
if b then
- let p = nf_evar evd ev in
+ let p = nf_evar evd (EConstr.Unsafe.to_constr ev) in
evd, p
else error_cannot_find_well_typed_abstraction env evd
c l None
@@ -184,8 +184,8 @@ let pose_all_metas_as_evars env evd t =
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
let src = Evd.evar_source_of_meta mv !evdref in
let ev = Evarutil.e_new_evar env evdref ~src ty in
- evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
- EConstr.of_constr ev)
+ evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
+ ev)
| _ ->
EConstr.map !evdref aux t in
let c = aux t in
@@ -1236,7 +1236,6 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma cty)) with
| Prod (_,c1,c2) ->
let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
- let evar = EConstr.of_constr evar in
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
| _ -> error "Apply_Head_Then"
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:48:16 +0000