aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml5
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/evarsolve.ml13
-rw-r--r--pretyping/evarutil.ml69
-rw-r--r--pretyping/evarutil.mli26
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/tacred.ml29
-rw-r--r--pretyping/tacred.mli3
-rw-r--r--pretyping/typeclasses.ml11
-rw-r--r--pretyping/typing.ml8
-rw-r--r--pretyping/typing.mli6
-rw-r--r--pretyping/unification.ml4
16 files changed, 119 insertions, 82 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index dd58590923..8a55a7aaa5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -28,6 +28,7 @@ open Evarutil
open Evarsolve
open Evarconv
open Evd
+open Sigma.Notations
open Context.Rel.Declaration
(* Pattern-matching errors *)
@@ -1955,8 +1956,10 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let sigma,t = match tycon with
| Some t -> sigma,t
| None ->
- let sigma, (t, _) =
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ 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, t
in
(* First strategy: we build an "inversion" predicate *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9d5a6006de..57b273d0d5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -189,7 +189,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
(subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some (fun x ->
let term = co x in
- Typing.solve_evars env evdref term)
+ Typing.e_solve_evars env evdref term)
in
if isEvar c || isEvar c' then
(* Second-order unification needed. *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 67a8f01aa4..c973e1cef3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -528,7 +528,10 @@ let rec detype flags avoid env sigma t =
in
let id,l =
try
- let id = Evd.evar_ident evk sigma in
+ let id = match Evd.evar_ident evk sigma with
+ | None -> Evd.pr_evar_suggested_name evk sigma
+ | Some id -> id
+ in
let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 020f998aa7..0a45ae9fd8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1013,7 +1013,9 @@ 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,ev = new_evar_instance sign !evdref evty ~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 ev),evty)::!evsref;
ev in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a65394e17b..3d1822102a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -19,6 +19,7 @@ open Retyping
open Reductionops
open Evarutil
open Pretype_errors
+open Sigma.Notations
open Context.Rel.Declaration
let normalize_evar evd ev =
@@ -182,7 +183,9 @@ let restrict_evar_key evd evk filter candidates =
let candidates = match candidates with
| NoUpdate -> evi.evar_candidates
| UpdateWith c -> Some c in
- restrict_evar evd evk filter candidates
+ 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)
end
(* Restrict an applied evar and returns its restriction in the same context *)
@@ -580,7 +583,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,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+ 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 t_in_env = whd_evar evd t_in_env in
let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
let ctxt = named_context_of_val sign in
@@ -643,8 +648,10 @@ 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,ev2_in_sign =
+ let evd = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (ev2_in_sign, evd, _) =
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 ev2_in_sign), Array.of_list inst2_in_env) in
(evd, ev2_in_sign, ev2_in_env)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 343d3ef903..ab70de0578 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -19,6 +19,7 @@ open Environ
open Evd
open Reductionops
open Pretype_errors
+open Sigma.Notations
(** Combinators *)
@@ -41,7 +42,7 @@ let e_new_global evdref x =
evd_comb1 (Evd.fresh_global (Global.env())) evdref x
let new_global evd x =
- Evd.fresh_global (Global.env()) evd x
+ Sigma.fresh_global (Global.env()) evd x
(****************************************************)
(* Expanding/testing/exposing existential variables *)
@@ -359,23 +360,19 @@ let push_rel_context_to_named_context env typ =
let default_source = (Loc.ghost,Evar_kinds.InternalHole)
let restrict_evar evd evk filter candidates =
+ let evd = Sigma.to_evar_map evd in
let evd, evk' = Evd.restrict evk filter ?candidates evd in
- Evd.declare_future_goal evk' evd, evk'
+ Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
let new_pure_evar_full evd evi =
+ let evd = Sigma.to_evar_map evd in
let (evd, evk) = Evd.new_evar evd evi in
let evd = Evd.declare_future_goal evk evd in
- (evd, evk)
+ Sigma.Unsafe.of_pair (evk, evd)
let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
- let default_naming =
- if principal then
- (* waiting for a more principled approach
- (unnamed evars, private names?) *)
- Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
- else
- Misctypes.IntroAnonymous
- in
+ let evd = Sigma.to_evar_map evd in
+ let default_naming = Misctypes.IntroAnonymous in
let naming = Option.default default_naming naming in
let evi = {
evar_hyps = sign;
@@ -391,17 +388,17 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
if principal then Evd.declare_principal_goal newevk evd
else Evd.declare_future_goal newevk evd
in
- (evd,newevk)
+ Sigma.Unsafe.of_pair (newevk, evd)
let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
- (evd,mkEvar (newevk,Array.of_list instance))
+ let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+ Sigma (mkEvar (newevk,Array.of_list instance), evd, p)
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
-let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
let instance =
@@ -410,24 +407,26 @@ let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal t
| Some filter -> Filter.filter_list filter instance in
new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
- let evd = Sigma.to_evar_map evd in
- let (sigma, c) = new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
- Sigma.Unsafe.of_pair (c, sigma)
+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 new_type_evar env evd ?src ?filter ?naming ?principal rigid =
- let evd', s = new_sort_variable rigid evd in
- let evd', e = new_evar_unsafe env evd' ?src ?filter ?naming ?principal (mkSort s) in
- evd', (e, s)
+ let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in
+ let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+ Sigma ((e, s), evd', p +> q)
let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
- let evd', c = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
- evdref := evd';
+ let sigma = Sigma.Unsafe.of_evar_map !evdref in
+ let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in
+ let sigma = Sigma.to_evar_map sigma in
+ evdref := sigma;
c
let new_Type ?(rigid=Evd.univ_flexible) env evd =
- let evd', s = new_sort_variable rigid evd in
- evd', mkSort s
+ let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in
+ Sigma (mkSort s, sigma, p)
let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
let evd', s = new_sort_variable rigid !evdref in
@@ -526,7 +525,9 @@ let rec check_and_clear_in_constr env evdref err ids c =
else
let origfilter = Evd.evar_filter evi in
let filter = Evd.Filter.apply_subfilter origfilter filter in
- let evd,_ = restrict_evar !evdref evk filter None in
+ let evd = Sigma.Unsafe.of_evar_map !evdref in
+ let Sigma (_, evd, _) = restrict_evar evd evk filter None in
+ let evd = Sigma.to_evar_map evd in
evdref := evd;
(* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
let evi = Evd.find !evdref evk in
@@ -734,7 +735,10 @@ let define_pure_evar_as_product evd evk =
let concl = whd_betadeltaiota evenv evd evi.evar_concl in
let s = destSort concl in
let evd1,(dom,u1) =
- new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+ 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)
+ in
let evd2,rng =
let newenv = push_named (LocalAssum (id, dom)) evenv in
let src = evar_source evk evd1 in
@@ -745,7 +749,10 @@ let define_pure_evar_as_product evd evk =
else
let status = univ_flexible_alg in
let evd3, (rng, srng) =
- new_type_evar newenv evd1 status ~src ~filter in
+ 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)
+ in
let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
evd3, rng
@@ -825,8 +832,8 @@ let define_evar_as_sort env evd (ev,args) =
any type has type Type. May cause some trouble, but not so far... *)
let judge_of_new_Type evd =
- let evd', s = new_univ_variable univ_rigid evd in
- evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
+ let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
+ Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
(* Propagation of constraints through application and abstraction:
Given a type constraint on a functional term, returns the type
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d87c7ef8d1..bc4c37a918 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -27,12 +27,12 @@ val new_evar :
?principal:bool -> types -> (constr, 'r) Sigma.sigma
val new_pure_evar :
- named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> types -> evar_map * evar
+ ?principal:bool -> types -> (evar, 'r) Sigma.sigma
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
+val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
(** the same with side-effects *)
val e_new_evar :
@@ -44,23 +44,23 @@ val e_new_evar :
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
- env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+ env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
- evar_map * (constr * sorts)
+ (constr * sorts, 'r) Sigma.sigma
val e_new_type_evar : env -> evar_map ref ->
?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
-val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
+val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
-val restrict_evar : evar_map -> existential_key -> Filter.t ->
- constr list option -> evar_map * existential_key
+val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
+ constr list option -> (existential_key, 'r) Sigma.sigma
(** Polymorphic constants *)
-val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
+val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
val e_new_global : evar_map ref -> Globnames.global_reference -> constr
(** Create a fresh evar in a context different from its definition context:
@@ -70,11 +70,11 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
of [inst] are typed in the occurrence context and their type (seen
as a telescope) is [sign] *)
val new_evar_instance :
- named_context_val -> evar_map -> types ->
- ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
+ named_context_val -> 'r Sigma.t -> types ->
+ ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool ->
- constr list -> evar_map * constr
+ constr list -> (constr, 'r) Sigma.sigma
val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
@@ -138,7 +138,7 @@ val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
(** {6 Value/Type constraints} *)
-val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
+val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
type type_constraint = types option
type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7c91b1a934..5e8c5beb58 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,6 +42,7 @@ open Glob_ops
open Evarconv
open Pattern
open Misctypes
+open Sigma.Notations
open Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
@@ -443,10 +444,13 @@ let pretype_sort evdref = function
| GType s -> evd_comb1 judge_of_Type evdref s
let new_type_evar env evdref loc =
- let e, s =
- evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
- univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
- in e
+ let sigma = Sigma.Unsafe.of_evar_map !evdref in
+ let Sigma ((e, _), sigma, _) =
+ Evarutil.new_type_evar env sigma
+ univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
+ in
+ evdref := Sigma.to_evar_map sigma;
+ e
let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d7637d1c27..935e18d8dd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -573,7 +573,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 = env -> evar_map -> constr -> evar_map * constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e65ab83b29..b38252e971 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -108,7 +108,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 = env -> evar_map -> constr -> evar_map * constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ae224cf0d4..7d2504004f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,6 +23,7 @@ open Reductionops
open Cbv
open Patternops
open Locus
+open Sigma.Notations
(* Errors *)
@@ -389,7 +390,9 @@ 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, evk) = Evarutil.new_pure_evar venv !evd dummy in
+ 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
evd := sigma;
minargs := Evar.Map.add evk min !minargs;
lift k (mkEvar (evk, [|fx;ref|]))
@@ -970,10 +973,12 @@ 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 g f acc c
-let e_contextually byhead (occs,c) f env sigma t =
+let e_contextually byhead (occs,c) f = { e_redfun = 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 =
if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t
@@ -992,8 +997,8 @@ let e_contextually byhead (occs,c) f env sigma t =
(* Skip inner occurrences for stable counting of occurrences *)
if locs != [] then
ignore (traverse_below (Some (!pos-1)) envc t);
- let evm, t = f subst env !evd t in
- (evd := evm; 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)
end
else
traverse_below nested envc t
@@ -1012,11 +1017,15 @@ let e_contextually byhead (occs,c) f 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;
- !evd, t'
+ Sigma.Unsafe.of_pair (t', !evd)
+ end }
let contextually byhead occs f env sigma t =
- let f' subst env sigma t = sigma, f subst env sigma t in
- snd (e_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
(* linear bindings (following pretty-printer) of the value of name in c.
* n is the number of the next occurrence of name.
@@ -1135,13 +1144,15 @@ let abstract_scheme env (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 env sigma c =
+let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
+ let sigma = Sigma.to_evar_map sigma in
let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
try
let _ = Typing.unsafe_type_of env sigma abstr_trm in
- sigma, applist(abstr_trm, List.map snd loccs_trm)
+ Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
with Type_errors.TypeError (env',t) ->
raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
+ end }
(* Used in several tactics. *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 6a7248e197..195b21bbf2 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -61,8 +61,7 @@ val unfoldn :
val fold_commands : constr list -> reduction_function
(** Pattern *)
-val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr ->
- evar_map * constr
+val pattern_occs : (occurrences * constr) list -> e_reduction_function
(** Rem: Lazy strategies are defined in Reduction *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 6c62bd08fc..0faa35c875 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -493,15 +493,18 @@ let is_instance = function
let resolvable = Store.field ()
let set_resolvable s b =
- Store.set s resolvable b
+ if b then Store.remove s resolvable
+ else Store.set s resolvable ()
let is_resolvable evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
- Option.default true (Store.get evi.evar_extra resolvable)
+ Option.is_empty (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- let t = Store.set evi.evar_extra resolvable b in
- { evi with evar_extra = t }
+ if is_resolvable evi = b then evi
+ else
+ let t = set_resolvable evi.evar_extra b in
+ { evi with evar_extra = t }
let mark_resolvability b evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8be28a6202..5347d965b5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -268,7 +268,7 @@ and execute_recdef env evdref (names,lar,vdef) =
and execute_array env evdref = Array.map (execute env evdref)
-let check env evdref c t =
+let e_check env evdref c t =
let env = enrich_env env evdref in
let j = execute env evdref c in
if not (Evarconv.e_cumul env evdref j.uj_type t) then
@@ -284,7 +284,7 @@ let unsafe_type_of env evd c =
(* Sort of a type *)
-let sort_of env evdref c =
+let e_sort_of env evdref c =
let env = enrich_env env evdref in
let j = execute env evdref c in
let a = e_type_judgment env evdref j in
@@ -311,10 +311,10 @@ let e_type_of ?(refresh=false) env evdref c =
c
else j.uj_type
-let solve_evars env evdref c =
+let e_solve_evars env evdref c =
let env = enrich_env env evdref in
let c = (execute env evdref c).uj_val in
(* side-effect on evdref *)
nf_evar !evdref c
-let _ = Evarconv.set_solve_evars solve_evars
+let _ = Evarconv.set_solve_evars e_solve_evars
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index dafd75231a..e524edcca8 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -24,16 +24,16 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
(** Typecheck a type and return its sort *)
-val sort_of : env -> evar_map ref -> types -> sorts
+val e_sort_of : env -> evar_map ref -> types -> sorts
(** Typecheck a term has a given type (assuming the type is OK) *)
-val check : env -> evar_map ref -> constr -> types -> unit
+val e_check : env -> evar_map ref -> constr -> types -> unit
(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
(** Solve existential variables using typing *)
-val solve_evars : env -> evar_map ref -> constr -> constr
+val e_solve_evars : env -> evar_map ref -> constr -> constr
(** Raise an error message if incorrect elimination for this inductive *)
(** (first constr is term to match, second is return predicate) *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6614749d08..e68961da74 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1473,9 +1473,7 @@ let default_matching_core_flags sigma =
check_applied_meta_types = true;
use_pattern_unification = false;
use_meta_bound_pattern_unification = false;
- frozen_evars =
- fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
- sigma Evar.Set.empty;
+ frozen_evars = Evar.Map.domain (Evd.undefined_map sigma);
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = false;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 20:47:19 +0000