aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--pretyping/evardefine.ml18
-rw-r--r--pretyping/evarsolve.ml13
-rw-r--r--pretyping/indrec.ml16
-rw-r--r--pretyping/indrec.mli8
-rw-r--r--pretyping/pretyping.ml27
-rw-r--r--pretyping/program.ml9
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/tacred.ml31
-rw-r--r--pretyping/unification.ml34
-rw-r--r--pretyping/unification.mli6
13 files changed, 65 insertions, 116 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index efab5b977..c3f392980 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -32,7 +32,6 @@ open Evardefine
open Evarsolve
open Evarconv
open Evd
-open Sigma.Notations
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -2000,10 +1999,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
let sigma,t = match tycon with
| Some t -> refresh_tycon sigma t
| None ->
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma ((t, _), sigma, _) =
+ let (sigma, (t, _)) =
new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
- let sigma = Sigma.to_evar_map sigma in
sigma, t
in
(* First strategy: we build an "inversion" predicate *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1d6b611da..3757ba7e6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -23,7 +23,6 @@ open Evardefine
open Evarsolve
open Evd
open Pretype_errors
-open Sigma.Notations
open Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
@@ -913,9 +912,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
(i,t2::ks, m-1, test)
else
let dloc = Loc.tag Evar_kinds.InternalHole in
- 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
+ let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
(i', ev :: ks, m - 1,test))
(evd,[],List.length bs,fun i -> Success i) bs
in
@@ -1099,9 +1096,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| None ->
let evty = set_holes evdref cty subst 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
+ let evd = !evdref in
+ let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
evdref := evd;
evsref := (fst (destEvar !evdref ev),evty)::!evsref;
ev in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index a11619846..2d86daadb 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -17,15 +17,9 @@ open Namegen
open Evd
open Evarutil
open Pretype_errors
-open Sigma.Notations
module RelDecl = Context.Rel.Declaration
-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
- (Sigma.to_evar_map evd, evk)
-
let env_nf_evar sigma env =
let nf_evar c = nf_evar sigma c in
process_rel_context
@@ -82,9 +76,7 @@ let define_pure_evar_as_product evd evk =
let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
let s = destSort evd concl in
let evd1,(dom,u1) =
- let evd = Sigma.Unsafe.of_evar_map evd in
- let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
- (Sigma.to_evar_map evd1, e)
+ new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi)
in
let evd2,rng =
let newenv = push_named (LocalAssum (id, dom)) evenv in
@@ -92,13 +84,11 @@ let define_pure_evar_as_product evd evk =
let filter = Filter.extend 1 (evar_filter evi) in
if is_prop_sort (ESorts.kind evd1 s) then
(* Impredicative product, conclusion must fall in [Prop]. *)
- new_evar_unsafe newenv evd1 concl ~src ~filter
+ new_evar newenv evd1 concl ~src ~filter
else
let status = univ_flexible_alg in
let evd3, (rng, srng) =
- let evd1 = Sigma.Unsafe.of_evar_map evd1 in
- let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
- (Sigma.to_evar_map evd3, e)
+ new_type_evar newenv evd1 status ~src ~filter
in
let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in
@@ -143,7 +133,7 @@ let define_pure_evar_as_lambda env evd evk =
let newenv = push_named (LocalAssum (id, dom)) evenv in
let filter = Filter.extend 1 (evar_filter evi) in
let src = evar_source evk evd1 in
- let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+ let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
let lam = mkLambda (Name id, dom, subst_var id body) in
Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index de5a62726..ff0aeff75 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -20,7 +20,6 @@ open Retyping
open Reductionops
open Evarutil
open Pretype_errors
-open Sigma.Notations
let normalize_evar evd ev =
match EConstr.kind evd (mkEvar ev) with
@@ -203,9 +202,7 @@ let restrict_evar_key evd evk filter candidates =
let candidates = match candidates with
| NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
| UpdateWith c -> Some c in
- let sigma = Sigma.Unsafe.of_evar_map evd in
- let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in
- (Sigma.to_evar_map sigma, evk)
+ restrict_evar evd evk filter candidates
end
(* Restrict an applied evar and returns its restriction in the same context *)
@@ -649,9 +646,7 @@ let make_projectable_subst aliases sigma evi args =
*)
let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
- let evd = Sigma.Unsafe.of_evar_map evd in
- let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
- let evd = Sigma.to_evar_map evd in
+ let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
let t_in_env = whd_evar evd t_in_env in
let (evk, _) = destEvar evd evar_in_env in
let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
@@ -721,10 +716,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
~status:univ_flexible (Some false) env evd (mkSort s) in
define_evar_from_virtual_equation define_fun env evd src ty_in_env
ty_t_in_sign sign2 filter2 inst2_in_env in
- let evd = Sigma.Unsafe.of_evar_map evd in
- let Sigma (ev2_in_sign, evd, _) =
+ let (evd, ev2_in_sign) =
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 ev2_in_sign), Array.of_list inst2_in_env) in
(evd, ev2_in_sign, ev2_in_env)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8a902f3a3..97aec1814 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -27,7 +27,6 @@ open Inductiveops
open Environ
open Reductionops
open Nametab
-open Sigma.Notations
open Context.Rel.Declaration
type dep_flag = bool
@@ -130,19 +129,19 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
it_mkLambda_or_LetIn_name env' obj deparsign
else
let cs = lift_constructor (k+1) constrs.(k) in
- let t = build_branch_type env (Sigma.to_evar_map sigma) dep (mkRel (k+1)) cs in
+ let t = build_branch_type env sigma dep (mkRel (k+1)) cs in
mkLambda_string "f" t
(add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1))
in
- let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
- let typP = make_arity env' (Sigma.to_evar_map sigma) dep indf s in
+ let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
+ let typP = make_arity env' sigma dep indf s in
let typP = EConstr.Unsafe.to_constr typP in
let c =
it_mkLambda_or_LetIn_name env
(mkLambda_string "P" typP
(add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar
in
- Sigma (c, sigma, p)
+ (sigma, c)
(* check if the type depends recursively on one of the inductive scheme *)
@@ -475,10 +474,9 @@ let mis_make_indrec env sigma listdepkind mib u =
it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
lnamesparrec
else
- let sigma = Sigma.Unsafe.of_evar_map !evdref in
- let Sigma (c, sigma, _) = mis_make_case_com dep env sigma (indi,u) (mibi,mipi) kind in
- let evd' = Sigma.to_evar_map sigma in
- evdref := evd'; c
+ let evd = !evdref in
+ let (evd, c) = mis_make_case_com dep env evd (indi,u) (mibi,mipi) kind in
+ evdref := evd; c
in
(* Body of mis_make_indrec *)
!evdref, List.init nrec make_one_rec
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 192b64a5e..a22470ae8 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -26,14 +26,14 @@ type dep_flag = bool
(** Build a case analysis elimination scheme in some sort family *)
-val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
- dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
+val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive ->
+ dep_flag -> sorts_family -> evar_map * Constr.t
(** Build a dependent case elimination predicate unless type is in Prop
or is a recursive record with primitive projections. *)
-val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
- sorts_family -> (constr, 'r) Sigma.sigma
+val build_case_analysis_scheme_default : env -> evar_map -> pinductive ->
+ sorts_family -> evar_map * Constr.t
(** Builds a recursive induction scheme (Peano-induction style) in the same
sort family as the inductive family; it is dependent if not in Prop
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 08a6dd4db..92e728683 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,8 +44,6 @@ open Glob_ops
open Evarconv
open Pattern
open Misctypes
-open Tactypes
-open Sigma.Notations
module NamedDecl = Context.Named.Declaration
@@ -111,9 +109,9 @@ let e_new_evar env evdref ?src ?naming typ =
let typ' = subst2 subst vsubst typ in
let instance = inst_rels @ inst_vars in
let sign = val_of_named_context nc in
- 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;
+ let sigma = !evdref in
+ let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in
+ evdref := sigma;
e
let push_rec_types sigma (lna,typarray,_) env =
@@ -390,9 +388,8 @@ let adjust_evar_source evdref na c =
begin match evi.evar_source with
| loc, Evar_kinds.QuestionMark (b,Anonymous) ->
let src = (loc,Evar_kinds.QuestionMark (b,na)) in
- let sigma = Sigma.Unsafe.of_evar_map !evdref in
- let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
- evdref := Sigma.to_evar_map evd;
+ let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in
+ evdref := evd;
mkEvar (evk',args)
| _ -> c
end
@@ -571,12 +568,12 @@ let pretype_sort ?loc evdref = function
| GType s -> evd_comb1 (judge_of_Type ?loc) evdref s
let new_type_evar env evdref loc =
- let sigma = Sigma.Unsafe.of_evar_map !evdref in
- let Sigma ((e, _), sigma, _) =
+ let sigma = !evdref in
+ let (sigma, (e, _)) =
Evarutil.new_type_evar env.ExtraEnv.env sigma
univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
in
- evdref := Sigma.to_evar_map sigma;
+ evdref := sigma;
e
module ConstrInterpObj =
@@ -1267,7 +1264,7 @@ let constr_flags = {
(* Fully evaluate an untyped constr *)
let type_uconstr ?(flags = constr_flags)
?(expected_type = WithoutTypeConstraint) ist c =
- { delayed = begin fun env sigma ->
+ begin fun env sigma ->
let { closure; term } = c in
let vars = {
ltac_constrs = closure.typed;
@@ -1275,10 +1272,8 @@ let type_uconstr ?(flags = constr_flags)
ltac_idents = closure.idents;
ltac_genargs = Id.Map.empty;
} in
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
- Sigma.Unsafe.of_pair (c, sigma)
- end }
+ understand_ltac flags env sigma vars expected_type term
+ end
let pretype k0 resolve_tc typcon env evdref lvar t =
pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 2fa3facb3..f9be82024 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -41,13 +41,8 @@ let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
let coq_not = init_reference ["Init";"Logic"] "not"
let coq_and = init_reference ["Init";"Logic"] "and"
-let new_global sigma gr =
- let open Sigma in
- let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr
- in Sigma.to_evar_map sigma, c
-
let mk_coq_not sigma x =
- let sigma, notc = new_global sigma (coq_not ()) in
+ let sigma, notc = Evarutil.new_global sigma (coq_not ()) in
sigma, EConstr.mkApp (notc, [| x |])
let unsafe_fold_right f = function
@@ -55,7 +50,7 @@ let unsafe_fold_right f = function
| [] -> invalid_arg "unsafe_fold_right"
let mk_coq_and sigma l =
- let sigma, and_typ = new_global sigma (coq_and ()) in
+ let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in
sigma, unsafe_fold_right
(fun c conj ->
EConstr.mkApp (and_typ, [| c ; conj |]))
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c976fe66d..b4654bfb5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -595,7 +595,7 @@ type state = constr * constr Stack.t
type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index af8048156..af0e28cdd 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -117,7 +117,7 @@ type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f2b0995b0..ec3669bfe 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -24,7 +24,6 @@ open Reductionops
open Cbv
open Patternops
open Locus
-open Sigma.Notations
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -399,9 +398,8 @@ let substl_with_function subst sigma constr =
if i <= k + Array.length v then
match v.(i-k-1) with
| (fx, Some (min, ref)) ->
- let sigma = Sigma.Unsafe.of_evar_map !evd in
- let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in
- let sigma = Sigma.to_evar_map sigma in
+ let sigma = !evd in
+ let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in
evd := sigma;
minargs := Evar.Map.add evk min !minargs;
Vars.lift k (mkEvar (evk, [|fx;ref|]))
@@ -983,11 +981,10 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
| _ -> mkApp (app', [| a' |]))
| _ -> 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 e_contextually byhead (occs,c) f = begin fun env sigma t ->
let (nowhere_except_in,locs) = Locusops.convert_occs occs in
let maxocc = List.fold_right max locs 0 in
let pos = ref 1 in
- let sigma = Sigma.to_evar_map sigma in
(** FIXME: we do suspicious things with this evarmap *)
let evd = ref sigma in
let rec traverse nested (env,c as envc) t =
@@ -1007,8 +1004,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
(* Skip inner occurrences for stable counting of occurrences *)
if locs != [] then
ignore (traverse_below (Some (!pos-1)) envc t);
- let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in
- (evd := Sigma.to_evar_map evm; t)
+ let (evm, t) = (f subst) env !evd t in
+ (evd := evm; t)
end
else
traverse_below nested envc t
@@ -1027,15 +1024,12 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
in
let t' = traverse None (env,c) t in
if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
- Sigma.Unsafe.of_pair (t', !evd)
- end }
+ (!evd, t')
+ end
let contextually byhead occs f env sigma t =
- let f' subst = { e_redfun = begin fun env sigma t ->
- Sigma.here (f subst env (Sigma.to_evar_map sigma) t) sigma
- end } in
- let Sigma (c, _, _) = (e_contextually byhead occs f').e_redfun env (Sigma.Unsafe.of_evar_map sigma) t in
- c
+ let f' subst env sigma t = sigma, f subst env sigma t in
+ snd (e_contextually byhead occs f' env sigma t)
(* linear bindings (following pretty-printer) of the value of name in c.
* n is the number of the next occurrence of name.
@@ -1154,15 +1148,14 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
mkLambda (na,ta,c'), sigma'
-let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
- let sigma = Sigma.to_evar_map sigma in
+let pattern_occs loccs_trm = begin fun env sigma c ->
let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
try
let _ = Typing.unsafe_type_of env sigma abstr_trm in
- Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
+ (sigma, applist(abstr_trm, List.map snd loccs_trm))
with Type_errors.TypeError (env',t) ->
raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
- end }
+ end
(* Used in several tactics. *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d1643a8c7..0fb48ed8c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -31,7 +31,6 @@ open Recordops
open Locus
open Locusops
open Find_subterm
-open Sigma.Notations
type metabinding = (metavariable * EConstr.constr * (instance_constraint * instance_typing_status))
@@ -145,9 +144,7 @@ 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 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) = new_evar env evd typ 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
@@ -1239,20 +1236,19 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
* close it off. But this might not always work,
* since other metavars might also need to be resolved. *)
-let applyHead env (type r) (evd : r Sigma.t) n c =
- let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma =
- fun n c cty p evd ->
+let applyHead env evd n c =
+ let rec apprec n c cty evd =
if Int.equal n 0 then
- Sigma (c, evd, p)
+ (evd, c)
else
- let sigma = Sigma.to_evar_map evd in
- match EConstr.kind sigma (whd_all env sigma cty) with
+ match EConstr.kind evd (whd_all env evd cty) with
| Prod (_,c1,c2) ->
- let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
- apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
+ let (evd',evar) =
+ Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
+ apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
| _ -> user_err Pp.(str "Apply_Head_Then")
in
- apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
+ apprec n c (Typing.unsafe_type_of env evd c) evd
let is_mimick_head sigma ts f =
match EConstr.kind sigma f with
@@ -1416,9 +1412,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
and mimick_undefined_evar evd flags hdc nargs sp =
let ev = Evd.find_undefined evd sp in
let sp_env = Global.env_of_context ev.evar_hyps in
- let evd = Sigma.Unsafe.of_evar_map evd in
- let Sigma (c, evd', _) = applyHead sp_env evd nargs hdc in
- let evd' = Sigma.to_evar_map evd' in
+ let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
(get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in
@@ -1534,10 +1528,9 @@ let indirectly_dependent sigma c d decls =
List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
- let current_sigma = Sigma.to_evar_map current_sigma in
let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
let sigma, subst = nf_univ_variables sigma in
- Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))), sigma)
+ (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
let default_matching_core_flags sigma =
let ts = Names.full_transparent_state in {
@@ -1684,7 +1677,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
let res = match out test with
| None -> None
- | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma))
+ | Some (sigma, c) -> Some (sigma,c)
in
(id,sign,depdecls,lastlhyp,ccl,res)
with
@@ -1711,10 +1704,9 @@ type abstraction_request =
type 'r abstraction_result =
Names.Id.t * named_context_val *
named_declaration list * Names.Id.t option *
- types * (constr, 'r) Sigma.sigma option
+ types * (evar_map * constr) option
let make_abstraction env evd ccl abs =
- let evd = Sigma.to_evar_map evd in
match abs with
| AbstractPattern (from_prefix,check,name,c,occs,check_occs) ->
make_abstraction_core name
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8d7e3521d..0d90ab158 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -76,14 +76,14 @@ type abstraction_request =
| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
- env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma
+ env -> evar_map -> (evar_map * constr) -> evar_map * constr
type 'r abstraction_result =
Names.Id.t * named_context_val *
named_declaration list * Names.Id.t option *
- types * (constr, 'r) Sigma.sigma option
+ types * (evar_map * constr) option
-val make_abstraction : env -> 'r Sigma.t -> constr ->
+val make_abstraction : env -> evar_map -> constr ->
abstraction_request -> 'r abstraction_result
val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 16:52:19 +0000