aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/sigma.ml12
-rw-r--r--engine/sigma.mli7
-rw-r--r--plugins/firstorder/instances.ml5
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/evarsolve.ml13
-rw-r--r--pretyping/evarutil.ml60
-rw-r--r--pretyping/evarutil.mli26
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/tacred.ml5
-rw-r--r--proofs/goal.ml11
-rw-r--r--tactics/rewrite.ml22
-rw-r--r--tactics/tactics.ml9
-rw-r--r--toplevel/record.ml9
14 files changed, 136 insertions, 64 deletions
diff --git a/engine/sigma.ml b/engine/sigma.ml
index e886b0d1e..c25aac0c1 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,6 +36,18 @@ let new_evar sigma ?naming info =
let define evk c sigma =
Sigma ((), Evd.define evk c sigma, ())
+let new_univ_level_variable ?name ?predicative rigid sigma =
+ let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in
+ Sigma (u, sigma, ())
+
+let new_univ_variable ?name ?predicative rigid sigma =
+ let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in
+ Sigma (u, sigma, ())
+
+let new_sort_variable ?name ?predicative rigid sigma =
+ let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in
+ Sigma (u, sigma, ())
+
let fresh_sort_in_family ?rigid env sigma s =
let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
Sigma (s, sigma, ())
diff --git a/engine/sigma.mli b/engine/sigma.mli
index cb948dba5..d7ae2e4ac 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -66,6 +66,13 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
(** Polymorphic universes *)
+val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+ 'r t -> (Univ.universe_level, 'r) sigma
+val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+ 'r t -> (Univ.universe, 'r) sigma
+val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
+ 'r t -> (Sorts.t, 'r) sigma
+
val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
val fresh_constant_instance :
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a717cc91e..fcbad46d4 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,6 +22,7 @@ open Formula
open Sequent
open Names
open Misctypes
+open Sigma.Notations
let compare_instance inst1 inst2=
match inst1,inst2 with
@@ -116,7 +117,9 @@ let mk_open_instance id idc gl m t=
let rec aux n avoid env evmap decls =
if Int.equal n 0 then evmap, decls else
let nid=(fresh_id avoid var_id gl) in
- let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ let evmap = Sigma.Unsafe.of_evar_map evmap in
+ let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ let evmap = Sigma.to_evar_map evmap in
let decl = (Name nid,None,c) in
aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m [] env evmap [] in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2cbf3a265..91bf11eb5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -28,6 +28,7 @@ open Evarutil
open Evarsolve
open Evarconv
open Evd
+open Sigma.Notations
(* Pattern-matching errors *)
@@ -1947,8 +1948,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/evarconv.ml b/pretyping/evarconv.ml
index 99e51330e..f3ff26876 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1007,7 +1007,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 0dd0ad2e0..518f4df40 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
let normalize_evar evd ev =
match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -180,7 +181,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 *)
@@ -570,7 +573,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
@@ -631,8 +636,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 cd5188cd7..2ed557683 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 *)
@@ -342,15 +343,18 @@ 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 evd = Sigma.to_evar_map evd in
let default_naming = Misctypes.IntroAnonymous in
let naming = Option.default default_naming naming in
let evi = {
@@ -367,17 +371,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 =
@@ -386,24 +390,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
@@ -501,7 +507,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
@@ -708,7 +716,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 (id, None, dom) evenv in
let src = evar_source evk evd1 in
@@ -719,7 +730,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
@@ -798,8 +812,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 d87c7ef8d..bc4c37a91 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 11fba7b94..835dc2f80 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
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = constr_under_binders Id.Map.t
@@ -444,10 +445,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/tacred.ml b/pretyping/tacred.ml
index bd46911c9..085aaf78a 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 *)
@@ -385,7 +386,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|]))
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 43a3024e5..1251dacd5 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,6 +9,7 @@
open Util
open Pp
open Term
+open Sigma.Notations
(* This module implements the abstract interface to goals *)
(* A general invariant of the module, is that a goal whose associated
@@ -70,7 +71,9 @@ module V82 = struct
Evd.evar_extra = extra }
in
let evi = Typeclasses.mark_unresolvable evi in
- let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
+ let evars = Sigma.Unsafe.of_evar_map evars in
+ let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in
+ let evars = Sigma.to_evar_map evars in
let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
let ctxt = Environ.named_context_of_val hyps in
let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
@@ -126,8 +129,10 @@ module V82 = struct
let new_evi =
{ evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
let new_evi = Typeclasses.mark_unresolvable new_evi in
- let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
- { Evd.it = evk ; sigma = new_sigma; }
+ let sigma = Sigma.Unsafe.of_evar_map Evd.empty in
+ let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in
+ let sigma = Sigma.to_evar_map sigma in
+ { Evd.it = evk ; sigma = sigma; }
(* Used by the compatibility layer and typeclasses *)
let nf_evar sigma gl =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 29002af9e..c50535a17 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -64,8 +64,10 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
let find_global dir s =
let gr = lazy (try_find_global_reference dir s) in
- fun (evd,cstrs) ->
- let evd, c = Evarutil.new_global evd (Lazy.force gr) in
+ fun (evd,cstrs) ->
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
+ let evd = Sigma.to_evar_map sigma in
(evd, cstrs), c
(** Utility for dealing with polymorphic applications *)
@@ -172,13 +174,17 @@ end) = struct
let proper_type =
let l = lazy (Lazy.force proper_class).cl_impl in
fun (evd,cstrs) ->
- let evd, c = Evarutil.new_global evd (Lazy.force l) in
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
+ let evd = Sigma.to_evar_map sigma in
(evd, cstrs), c
let proper_proxy_type =
let l = lazy (Lazy.force proper_proxy_class).cl_impl in
fun (evd,cstrs) ->
- let evd, c = Evarutil.new_global evd (Lazy.force l) in
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
+ let evd = Sigma.to_evar_map sigma in
(evd, cstrs), c
let proper_proof env evars carrier relation x =
@@ -347,7 +353,9 @@ end) = struct
(try
let params, args = Array.chop (Array.length args - 2) args in
let env' = Environ.push_rel_context rels env in
- let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+ let evars = Sigma.to_evar_map sigma in
let evars, inst =
app_poly env (evars,Evar.Set.empty)
rewrite_relation_class [| evar; mkApp (c, params) |] in
@@ -407,7 +415,9 @@ module TypeGlobal = struct
let inverse env (evd,cstrs) car rel =
- let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+ let sigma = Sigma.Unsafe.of_evar_map evd in
+ let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in
+ let evd = Sigma.to_evar_map sigma in
app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aeb3726a0..46e879854 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,14 +163,13 @@ let _ =
does not check anything. *)
let unsafe_intro env store (id, c, t) b =
Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
let ctx = named_context_val env in
let nctx = push_named_context_val (id, c, t) ctx in
let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar id) b in
- let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
- Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
+ let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+ Sigma (mkNamedLambda_or_LetIn (id, c, t) ev, sigma, p)
end }
let introduction ?(check=true) id =
@@ -344,9 +343,7 @@ let rename_hyp repl =
let nctx = Environ.val_of_named_context nhyps in
let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
- Sigma.Unsafe.of_pair (c, sigma)
+ Evarutil.new_evar_instance nctx sigma nconcl ~store instance
end }
end }
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 7ae203034..480e97169 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -24,6 +24,7 @@ open Type_errors
open Constrexpr
open Constrexpr_ops
open Goptions
+open Sigma.Notations
(********** definition d'un record (structure) **************)
@@ -336,11 +337,15 @@ let structure_signature ctx =
match l with [] -> Evd.empty
| [(_,_,typ)] ->
let env = Environ.empty_named_context_val in
- let (evm, _) = Evarutil.new_pure_evar env evm typ in
+ let evm = Sigma.Unsafe.of_evar_map evm in
+ let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm typ in
+ let evm = Sigma.to_evar_map evm in
evm
| (_,_,typ)::tl ->
let env = Environ.empty_named_context_val in
- let (evm, ev) = Evarutil.new_pure_evar env evm typ in
+ let evm = Sigma.Unsafe.of_evar_map evm in
+ let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm typ in
+ let evm = Sigma.to_evar_map evm in
let new_tl = Util.List.map_i
(fun pos (n,c,t) -> n,c,
Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 16:09:40 +0000