aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml13
-rw-r--r--engine/eConstr.mli4
-rw-r--r--engine/engine.mllib2
-rw-r--r--engine/evarutil.ml4
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/namegen.ml13
-rw-r--r--engine/termops.ml19
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml15
-rw-r--r--engine/uState.mli11
-rw-r--r--engine/univGen.ml212
-rw-r--r--engine/univGen.mli23
-rw-r--r--engine/univNames.ml2
-rw-r--r--engine/univops.ml28
-rw-r--r--engine/univops.mli6
15 files changed, 145 insertions, 211 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8ab3ce821e..3385b78958 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -74,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f)
let mkProj (p, c) = of_kind (Proj (p, c))
let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+let mkRef (gr,u) = let open GlobRef in match gr with
+ | ConstRef c -> mkConstU (c,u)
+ | IndRef ind -> mkIndU (ind,u)
+ | ConstructRef c -> mkConstructU (c,u)
+ | VarRef x -> mkVar x
+
let applist (f, arg) = mkApp (f, Array.of_list arg)
let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
@@ -166,6 +172,13 @@ let destProj sigma c = match kind sigma c with
| Proj (p, c) -> (p, c)
| _ -> raise DestKO
+let destRef sigma c = let open GlobRef in match kind sigma c with
+ | Var x -> VarRef x, EInstance.empty
+ | Const (c,u) -> ConstRef c, u
+ | Ind (ind,u) -> IndRef ind, u
+ | Construct (c,u) -> ConstructRef c, u
+ | _ -> raise DestKO
+
let decompose_app sigma c =
match kind sigma c with
| App (f,cl) -> (f, Array.to_list cl)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..1edc0ee12b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> t -> t
+val mkRef : GlobRef.t * EInstance.t -> t
+
val applist : t * t list -> t
val mkProd_or_LetIn : rel_declaration -> t -> t
@@ -180,6 +182,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
val decompose_app : Evd.evar_map -> t -> t * t list
(** Pops lambda abstractions until there are no more, skipping casts. *)
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 37e83b6238..bb43808542 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,8 +4,8 @@ UnivSubst
UnivProblem
UnivMinim
Universes
-Univops
UState
+Univops
Nameops
Evar_kinds
Evd
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fc2189f870..f9d9ce3569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -549,7 +549,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
if Id.Set.mem id' ids then
raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
in
- Id.Set.iter check (Environ.vars_of_global env c)
+ Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
in
c
@@ -579,7 +579,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
has dependencies in another hyp of the context of ev
and transitively remember the dependency *)
let check id _ =
- if occur_var_in_decl (Global.env ()) !evdref id h
+ if occur_var_in_decl env !evdref id h
then raise (Depends id)
in
let () = Id.Map.iter check ri in
diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..eafdc4cb46 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -818,7 +818,7 @@ let fresh_constructor_instance ?loc env evd c =
with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
- with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+ with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
let is_sort_variable evd s = UState.is_sort_variable evd.universes s
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7ce759a3fb..db72dc8ec3 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -21,7 +21,6 @@ open Constr
open Environ
open EConstr
open Vars
-open Nametab
open Nameops
open Libnames
open Globnames
@@ -82,14 +81,14 @@ let is_imported_ref = function
let is_global id =
try
- let ref = locate (qualid_of_ident id) in
+ let ref = Nametab.locate (qualid_of_ident id) in
not (is_imported_ref ref)
with Not_found ->
false
let is_constructor id =
try
- match locate (qualid_of_ident id) with
+ match Nametab.locate (qualid_of_ident id) with
| ConstructRef _ -> true
| _ -> false
with Not_found ->
@@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
| Cast (c,_,_) | App (c,_) -> hdrec c
| Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
| Const _ | Ind _ | Construct _ | Var _ as c ->
- Some (basename_of_global (global_of_constr c))
+ Some (Nametab.basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
Some (match lna.(i) with Name id -> id | _ -> assert false)
| Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None
@@ -148,8 +147,8 @@ let hdchar env sigma c =
| Cast (c,_,_) | App (c,_) -> hdrec k c
| Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
| Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
- | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
- | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
| Var id -> lowercase_first_char id
| Sort s -> sort_hdchar (ESorts.kind sigma s)
| Rel n ->
@@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) =
begin
try
let gseen = GlobRef.Set_env.add g gseen in
- let short = shortest_qualid_of_global Id.Set.empty g in
+ let short = Nametab.shortest_qualid_of_global Id.Set.empty g in
let dir, id = repr_qualid short in
let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in
accu := (gseen, vseen, ids)
diff --git a/engine/termops.ml b/engine/termops.ml
index 13bd8f7718..e1f5fb0d7f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -897,9 +897,9 @@ let occur_in_global env id constr =
let occur_var env sigma id c =
let rec occur_rec c =
- match EConstr.kind sigma c with
- | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
- | _ -> EConstr.iter sigma occur_rec c
+ match EConstr.destRef sigma c with
+ | gr, _ -> occur_in_global env id gr
+ | exception DestKO -> EConstr.iter sigma occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -946,9 +946,7 @@ let collect_vars sigma c =
| _ -> EConstr.fold sigma aux vars c in
aux Id.Set.empty c
-let vars_of_global_reference env gr =
- let c, _ = Global.constr_of_global_in_context env gr in
- vars_of_global (Global.env ()) c
+let vars_of_global_reference = vars_of_global
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
@@ -1443,12 +1441,9 @@ let clear_named_body id env =
let global_vars_set env sigma constr =
let rec filtrec acc c =
- let acc = match EConstr.kind sigma c with
- | Var _ | Const _ | Ind _ | Construct _ ->
- Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
- | _ -> acc
- in
- EConstr.fold sigma filtrec acc c
+ match EConstr.destRef sigma c with
+ | gr, _ -> Id.Set.union (vars_of_global env gr) acc
+ | exception DestKO -> EConstr.fold sigma filtrec acc c
in
filtrec Id.Set.empty constr
diff --git a/engine/termops.mli b/engine/termops.mli
index 64e3977d68..f7b9469ae8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -118,7 +118,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
val count_occurrences : Evd.evar_map -> constr -> constr -> int
val collect_metas : Evd.evar_map -> constr -> int list
val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
+
val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
+[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
diff --git a/engine/uState.ml b/engine/uState.ml
index 29cb3c9bcc..aa7ec63a6f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -406,12 +406,25 @@ let check_univ_decl ~poly uctx decl =
(Univ.ContextSet.constraints uctx.uctx_local);
ctx
+let restrict_universe_context (univs, csts) keep =
+ let open Univ in
+ let removed = LSet.diff univs keep in
+ if LSet.is_empty removed then univs, csts
+ else
+ let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+ let g = UGraph.empty_universes in
+ let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+ let g = UGraph.merge_constraints csts g in
+ let allkept = LSet.diff allunivs removed in
+ let csts = UGraph.constraints_for ~kept:allkept g in
+ (LSet.inter univs keep, csts)
+
let restrict ctx vars =
let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
(fst ctx.uctx_names) vars
in
- let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
+ let uctx' = restrict_universe_context ctx.uctx_local vars in
{ ctx with uctx_local = uctx' }
let demote_seff_univs entry uctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index f833508ebf..8053a7bf83 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,6 +13,7 @@
primitives when needed. *)
open Names
+open Univ
exception UniversesDiffer
@@ -91,6 +92,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
(** {5 Unification} *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+ the universes in [keep]. The constraints [csts] are adjusted so
+ that transitive constraints between remaining universes (those in
+ [keep] and those not in [univs]) are preserved. *)
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+
+(** [restrict uctx ctx] restricts the local universes of [uctx] to
+ [ctx] extended by local named universes and side effect universes
+ (from [demote_seff_univs]). Transitive constraints between retained
+ universes are preserved. *)
val restrict : t -> Univ.LSet.t -> t
val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b07d4848ff..130aa06f53 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -11,7 +11,6 @@
open Sorts
open Names
open Constr
-open Environ
open Univ
(* Generator of levels *)
@@ -32,122 +31,62 @@ let new_univ dp = Univ.Universe.make (new_univ_level dp)
let new_Type dp = mkType (new_univ dp)
let new_Type_sort dp = Type (new_univ dp)
-let fresh_universe_instance ctx =
- let init _ = new_univ_level () in
- Instance.of_array (Array.init (AUContext.size ctx) init)
+let fresh_instance auctx =
+ let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+ let ctx = Array.fold_right LSet.add inst LSet.empty in
+ let inst = Instance.of_array inst in
+ inst, (ctx, AUContext.instantiate inst auctx)
-let fresh_instance_from_context ctx =
- let inst = fresh_universe_instance ctx in
- let constraints = AUContext.instantiate inst ctx in
- inst, constraints
-
-let fresh_instance ctx =
- let ctx' = ref LSet.empty in
- let init _ =
- let u = new_univ_level () in
- ctx' := LSet.add u !ctx'; u
- in
- let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
- in !ctx', inst
-
-let existing_instance ctx inst =
+let existing_instance ?loc auctx inst =
let () =
let len1 = Array.length (Instance.to_array inst)
- and len2 = AUContext.size ctx in
+ and len2 = AUContext.size auctx in
if not (len1 == len2) then
- CErrors.user_err ~hdr:"Universes"
- Pp.(str "Polymorphic constant expected " ++ int len2 ++
- str" levels but was given " ++ int len1)
+ CErrors.user_err ?loc ~hdr:"Universes"
+ Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
else ()
- in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
- let ctx', inst =
- match inst with
- | Some inst -> existing_instance ctx inst
- | None -> fresh_instance ctx
in
- let constraints = AUContext.instantiate inst ctx in
- inst, (ctx', constraints)
+ inst, (LSet.empty, AUContext.instantiate inst auctx)
-(** Fresh universe polymorphic construction *)
+let fresh_instance_from ?loc ctx = function
+ | Some inst -> existing_instance ?loc ctx inst
+ | None -> fresh_instance ctx
-let fresh_constant_instance env c inst =
- let cb = lookup_constant c env in
- match cb.Declarations.const_universes with
- | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_const auctx ->
- let inst, ctx =
- fresh_instance_from auctx inst
- in
- ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- ((ind,Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_ind uactx ->
- let inst, ctx = (fresh_instance_from uactx) inst in
- ((ind,inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx =
- fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
- in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx inst in
- (((ind,i),inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
- (((ind,i),inst), ctx)
+(** Fresh universe polymorphic construction *)
open Globnames
-let fresh_global_instance ?names env gr =
- match gr with
- | VarRef id -> mkVar id, ContextSet.empty
- | ConstRef sp ->
- let c, ctx = fresh_constant_instance env sp names in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = fresh_constructor_instance env sp names in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = fresh_inductive_instance env sp names in
- mkIndU c, ctx
-
-let fresh_constant_instance env sp =
- fresh_constant_instance env sp None
-
-let fresh_inductive_instance env sp =
- fresh_inductive_instance env sp None
-
-let fresh_constructor_instance env sp =
- fresh_constructor_instance env sp None
-
-let constr_of_global gr =
- let c, ctx = fresh_global_instance (Global.env ()) gr in
- if not (Univ.ContextSet.is_empty ctx) then
- if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
- (* Should be an error as we might forget constraints, allow for now
- to make firstorder work with "using" clauses *)
- c
- else CErrors.user_err ~hdr:"constr_of_global"
- Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
- str " would forget universes.")
- else c
-
-let constr_of_global_univ (gr,u) =
- match gr with
- | VarRef id -> mkVar id
- | ConstRef sp -> mkConstU (sp,u)
- | ConstructRef sp -> mkConstructU (sp,u)
- | IndRef sp -> mkIndU (sp,u)
+let fresh_global_instance ?loc ?names env gr =
+ let auctx = Environ.universes_of_global env gr in
+ let u, ctx = fresh_instance_from ?loc auctx names in
+ u, ctx
+
+let fresh_constant_instance env c =
+ let u, ctx = fresh_global_instance env (ConstRef c) in
+ (c, u), ctx
+
+let fresh_inductive_instance env ind =
+ let u, ctx = fresh_global_instance env (IndRef ind) in
+ (ind, u), ctx
+
+let fresh_constructor_instance env c =
+ let u, ctx = fresh_global_instance env (ConstructRef c) in
+ (c, u), ctx
+
+let fresh_global_instance ?loc ?names env gr =
+ let u, ctx = fresh_global_instance ?loc ?names env gr in
+ mkRef (gr, u), ctx
+
+let constr_of_monomorphic_global gr =
+ if not (Global.is_polymorphic gr) then
+ fst (fresh_global_instance (Global.env ()) gr)
+ else CErrors.user_err ~hdr:"constr_of_global"
+ Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
+ str " would forget universes.")
+
+let constr_of_global gr = constr_of_monomorphic_global gr
+
+let constr_of_global_univ = mkRef
let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
@@ -166,52 +105,26 @@ open Declarations
let type_of_reference env r =
match r with
| VarRef id -> Environ.named_type id env, ContextSet.empty
+
| ConstRef c ->
let cb = Environ.lookup_constant c env in
let ty = cb.const_type in
- begin
- match cb.const_universes with
- | Monomorphic_const _ -> ty, ContextSet.empty
- | Polymorphic_const auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- Vars.subst_instance_constr inst ty, ctx
- end
+ let auctx = Declareops.constant_polymorphic_context cb in
+ let inst, ctx = fresh_instance auctx in
+ Vars.subst_instance_constr inst ty, ctx
+
| IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- begin
- match mib.mind_universes with
- | Monomorphic_ind _ ->
- let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
- ty, ContextSet.empty
- | Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- | Cumulative_ind cumi ->
- let inst, ctx =
- fresh_instance_from (ACumulativityInfo.univ_context cumi) None
- in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- end
-
- | ConstructRef cstr ->
- let (mib,oib as specif) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
- in
- begin
- match mib.mind_universes with
- | Monomorphic_ind _ ->
- Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
- | Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- | Cumulative_ind cumi ->
- let inst, ctx =
- fresh_instance_from (ACumulativityInfo.univ_context cumi) None
- in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- end
+ let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
+ let auctx = Declareops.inductive_polymorphic_context mib in
+ let inst, ctx = fresh_instance auctx in
+ let ty = Inductive.type_of_inductive env (specif, inst) in
+ ty, ctx
+
+ | ConstructRef (ind,_ as cstr) ->
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let auctx = Declareops.inductive_polymorphic_context mib in
+ let inst, ctx = fresh_instance auctx in
+ Inductive.type_of_constructor (cstr,inst) specif, ctx
let type_of_global t = type_of_reference (Global.env ()) t
@@ -225,8 +138,7 @@ let fresh_sort_in_family = function
let new_sort_in_family sf =
fst (fresh_sort_in_family sf)
-let extend_context (a, ctx) (ctx') =
- (a, ContextSet.union ctx ctx')
+let extend_context = Univ.extend_in_context_set
let new_global_univ () =
let u = fresh_level () in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 439424934c..42756701dc 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -23,20 +23,24 @@ val set_remote_new_univ_id : universe_id RemoteCounter.installer
val new_univ_id : unit -> universe_id
val new_univ_level : unit -> Level.t
+
val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_Type : unit -> types
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_global_univ : unit -> Universe.t in_universe_context_set
val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
-val fresh_instance_from_context : AUContext.t ->
- Instance.t constrained
+val fresh_instance : AUContext.t -> Instance.t in_universe_context_set
-val fresh_instance_from : AUContext.t -> Instance.t option ->
+val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
Instance.t in_universe_context_set
val fresh_sort_in_family : Sorts.family ->
@@ -48,7 +52,7 @@ val fresh_inductive_instance : env -> inductive ->
val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
constr in_universe_context_set
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
@@ -63,16 +67,23 @@ val fresh_universe_context_set_instance : ContextSet.t ->
val global_of_constr : constr -> GlobRef.t puniverses
val constr_of_global_univ : GlobRef.t puniverses -> constr
+[@@ocaml.deprecated "Use [Constr.mkRef]"]
val extend_context : 'a in_universe_context_set -> ContextSet.t ->
'a in_universe_context_set
+[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
(** Create a fresh global in the global environment, without side effects.
- BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
+ BEWARE: this raises an error on polymorphic constants/inductives:
the constraints should be properly added to an evd.
See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
- the proper way to get a fresh copy of a global reference. *)
+ the proper way to get a fresh copy of a polymorphic global reference. *)
+val constr_of_monomorphic_global : GlobRef.t -> constr
+
val constr_of_global : GlobRef.t -> constr
+[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
+ use [constr_of_monomorphic_global] if the reference is guaranteed to\
+ be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
(** Returns the type of the global reference, by creating a fresh instance of polymorphic
references and computing their instantiated universe context. (side-effect on the
diff --git a/engine/univNames.ml b/engine/univNames.ml
index e89dcedb9c..a71f9c5736 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -86,7 +86,7 @@ let register_universe_binders ref ubinders =
part of the code that depends on the internal representation of names in
abstract contexts, but removing it requires quite a rework of the
callers. *)
- let univs = AUContext.instance (Global.universes_of_global ref) in
+ let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
let map lvl =
try LMap.find lvl revmap
diff --git a/engine/univops.ml b/engine/univops.ml
index 7f9672f828..53c42023ad 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -8,30 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Univ
-open Constr
+let universes_of_constr = Vars.universes_of_constr
-let universes_of_constr c =
- let rec aux s c =
- match kind c with
- | Const (c, u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Sort u when not (Sorts.is_small u) ->
- let u = Sorts.univ_of_sort u in
- LSet.fold LSet.add (Universe.levels u) s
- | _ -> Constr.fold aux s c
- in aux LSet.empty c
-
-let restrict_universe_context (univs, csts) keep =
- let removed = LSet.diff univs keep in
- if LSet.is_empty removed then univs, csts
- else
- let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
- let g = UGraph.empty_universes in
- let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
- let g = UGraph.merge_constraints csts g in
- let allkept = LSet.diff allunivs removed in
- let csts = UGraph.constraints_for ~kept:allkept g in
- (LSet.inter univs keep, csts)
+let restrict_universe_context = UState.restrict_universe_context
diff --git a/engine/univops.mli b/engine/univops.mli
index 57a53597b9..597d2d6785 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -13,9 +13,7 @@ open Univ
(** Return the set of all universes appearing in [constr]. *)
val universes_of_constr : constr -> LSet.t
+[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
- the universes in [keep]. The constraints [csts] are adjusted so
- that transitive constraints between remaining universes (those in
- [keep] and those not in [univs]) are preserved. *)
val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:59:35 +0000