aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml2
-rw-r--r--engine/engine.mllib1
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/termops.ml2
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli4
-rw-r--r--engine/univNames.ml105
-rw-r--r--engine/univNames.mli41
-rw-r--r--engine/universes.ml117
-rw-r--r--engine/universes.mli67
-rw-r--r--interp/declare.ml6
-rw-r--r--interp/declare.mli2
-rw-r--r--pretyping/vernacexpr.ml8
-rw-r--r--printing/prettyp.ml8
-rw-r--r--printing/prettyp.mli8
-rw-r--r--printing/printer.ml2
-rw-r--r--printing/printmod.ml4
-rw-r--r--printing/printmod.mli2
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comInductive.mli4
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declareDef.mli4
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/record.ml8
-rw-r--r--vernac/record.mli2
-rw-r--r--vernac/vernacentries.ml2
29 files changed, 253 insertions, 172 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8d5b5bef4..b18cbbd7b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -203,7 +203,7 @@ let pproof p = pp(Proof.pr_proof p)
let ppuni u = pp(Universe.pr u)
let ppuni_level u = pp (Level.pr u)
-let prlev = Universes.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes
let ppuniverse_set l = pp (LSet.pr prlev l)
let ppuniverse_instance l = pp (Instance.pr prlev l)
let ppuniverse_context l = pp (pr_universe_context prlev l)
diff --git a/engine/engine.mllib b/engine/engine.mllib
index a5df5a9fa..207dbde1e 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,3 +1,4 @@
+UnivNames
Universes
Univops
UState
diff --git a/engine/evd.mli b/engine/evd.mli
index 509db525d..7ce525744 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -550,7 +550,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
val evar_universe_context_of_binders :
- Universes.universe_binders -> UState.t
+ UnivNames.universe_binders -> UState.t
[@@ocaml.deprecated "Alias of UState.of_binders"]
val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
@@ -559,7 +559,7 @@ val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
-val universe_binders : evar_map -> Universes.universe_binders
+val universe_binders : evar_map -> UnivNames.universe_binders
val add_constraints_context : UState.t ->
Univ.Constraint.t -> UState.t
[@@ocaml.deprecated "Alias of UState.add_constraints"]
diff --git a/engine/termops.ml b/engine/termops.ml
index df43be28e..9e975da58 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -47,7 +47,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
let pr_puniverses p u =
if Univ.Instance.is_empty u then p
- else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+ else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
let rec pr_constr c = match kind c with
| Rel n -> str "#"++int n
diff --git a/engine/uState.ml b/engine/uState.ml
index df50bae86..ffb54d441 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -24,7 +24,7 @@ module UPairSet = Universes.UPairSet
(* 2nd part used to check consistency on the fly. *)
type t =
- { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t;
+ { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t;
uctx_local : Univ.ContextSet.t; (** The local context of variables *)
uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *)
uctx_univ_variables : Universes.universe_opt_subst;
@@ -298,7 +298,7 @@ let reference_of_level uctx =
fun l ->
try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname)
with Not_found | Option.IsNone ->
- Universes.reference_of_level l
+ UnivNames.reference_of_level l
let pr_uctx_level uctx l =
Libnames.pr_reference (reference_of_level uctx l)
diff --git a/engine/uState.mli b/engine/uState.mli
index 48c38fafc..b1fcefb0a 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -34,9 +34,9 @@ val union : t -> t -> t
val of_context_set : Univ.ContextSet.t -> t
-val of_binders : Universes.universe_binders -> t
+val of_binders : UnivNames.universe_binders -> t
-val universe_binders : t -> Universes.universe_binders
+val universe_binders : t -> UnivNames.universe_binders
(** {5 Projections} *)
diff --git a/engine/univNames.ml b/engine/univNames.ml
new file mode 100644
index 000000000..6e59a7c9e
--- /dev/null
+++ b/engine/univNames.ml
@@ -0,0 +1,105 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Univ
+open Globnames
+open Nametab
+
+
+let reference_of_level l = CAst.make @@
+ match Level.name l with
+ | Some (d, n as na) ->
+ let qid =
+ try Nametab.shortest_qualid_of_universe na
+ with Not_found ->
+ let name = Id.of_string_soft (string_of_int n) in
+ Libnames.make_qualid d name
+ in Libnames.Qualid qid
+ | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
+
+let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
+
+(** Global universe information outside the kernel, to handle
+ polymorphic universe names in sections that have to be discharged. *)
+
+let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
+
+let add_global_universe u p =
+ match Level.name u with
+ | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
+ | None -> ()
+
+let is_polymorphic l =
+ match Level.name l with
+ | Some n ->
+ (try Nametab.UnivIdMap.find n !universe_map
+ with Not_found -> false)
+ | None -> false
+
+(** Local universe names of polymorphic references *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+let empty_binders = Id.Map.empty
+
+let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
+
+let universe_binders_of_global ref : universe_binders =
+ try
+ let l = Refmap.find ref !universe_binders_table in l
+ with Not_found -> Names.Id.Map.empty
+
+let cache_ubinder (_,(ref,l)) =
+ universe_binders_table := Refmap.add ref l !universe_binders_table
+
+let subst_ubinder (subst,(ref,l as orig)) =
+ let ref' = fst (Globnames.subst_global subst ref) in
+ if ref == ref' then orig else ref', l
+
+let discharge_ubinder (_,(ref,l)) =
+ Some (Lib.discharge_global ref, l)
+
+let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+ let open Libobject in
+ declare_object { (default_object "universe binder") with
+ cache_function = cache_ubinder;
+ load_function = (fun _ x -> cache_ubinder x);
+ classify_function = (fun x -> Substitute x);
+ subst_function = subst_ubinder;
+ discharge_function = discharge_ubinder;
+ rebuild_function = (fun x -> x); }
+
+let register_universe_binders ref ubinders =
+ (* Add the polymorphic (section) universes *)
+ let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
+ let qid = Nametab.shortest_qualid_of_universe lvl in
+ let level = Level.make (fst lvl) (snd lvl) in
+ if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
+ else ubinders)
+ !universe_map ubinders
+ in
+ if not (Id.Map.is_empty ubinders)
+ then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+
+type univ_name_list = Misctypes.lname list
+
+let universe_binders_with_opt_names ref levels = function
+ | None -> universe_binders_of_global ref
+ | Some udecl ->
+ if Int.equal(List.length levels) (List.length udecl)
+ then
+ List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
+ | Anonymous -> acc
+ | Name na -> Names.Id.Map.add na lvl acc)
+ empty_binders udecl levels
+ else
+ CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+ Pp.(str "Universe instance should have length " ++ int (List.length levels))
diff --git a/engine/univNames.mli b/engine/univNames.mli
new file mode 100644
index 000000000..e3bc3193d
--- /dev/null
+++ b/engine/univNames.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Univ
+
+val pr_with_global_universes : Level.t -> Pp.t
+val reference_of_level : Level.t -> Libnames.reference
+
+(** Global universe information outside the kernel, to handle
+ polymorphic universes in sections that have to be discharged. *)
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+
+(** Is [lvl] a global polymorphic universe? (ie section polymorphic universe) *)
+val is_polymorphic : Level.t -> bool
+
+(** Local universe name <-> level mapping *)
+
+type universe_binders = Univ.Level.t Names.Id.Map.t
+
+val empty_binders : universe_binders
+
+val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
+val universe_binders_of_global : Names.GlobRef.t -> universe_binders
+
+type univ_name_list = Misctypes.lname list
+
+(** [universe_binders_with_opt_names ref u l]
+
+ If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+ May error if the lengths mismatch.
+
+ Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Names.GlobRef.t ->
+ Univ.Level.t list -> univ_name_list option -> universe_binders
diff --git a/engine/universes.ml b/engine/universes.ml
index 96d49361f..1dccde025 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -15,102 +15,6 @@ open Names
open Constr
open Environ
open Univ
-open Globnames
-open Nametab
-
-module UPairs = OrderedType.UnorderedPair(Univ.Level)
-module UPairSet = Set.Make (UPairs)
-
-let reference_of_level l = CAst.make @@
- match Level.name l with
- | Some (d, n as na) ->
- let qid =
- try Nametab.shortest_qualid_of_universe na
- with Not_found ->
- let name = Id.of_string_soft (string_of_int n) in
- Libnames.make_qualid d name
- in Libnames.Qualid qid
- | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l))
-
-let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l)
-
-(** Global universe information outside the kernel, to handle
- polymorphic universe names in sections that have to be discharged. *)
-
-let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref)
-
-let add_global_universe u p =
- match Level.name u with
- | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map
- | None -> ()
-
-let is_polymorphic l =
- match Level.name l with
- | Some n ->
- (try Nametab.UnivIdMap.find n !universe_map
- with Not_found -> false)
- | None -> false
-
-(** Local universe names of polymorphic references *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
-
-let empty_binders = Id.Map.empty
-
-let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
-
-let universe_binders_of_global ref : universe_binders =
- try
- let l = Refmap.find ref !universe_binders_table in l
- with Not_found -> Names.Id.Map.empty
-
-let cache_ubinder (_,(ref,l)) =
- universe_binders_table := Refmap.add ref l !universe_binders_table
-
-let subst_ubinder (subst,(ref,l as orig)) =
- let ref' = fst (Globnames.subst_global subst ref) in
- if ref == ref' then orig else ref', l
-
-let discharge_ubinder (_,(ref,l)) =
- Some (Lib.discharge_global ref, l)
-
-let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
- let open Libobject in
- declare_object { (default_object "universe binder") with
- cache_function = cache_ubinder;
- load_function = (fun _ x -> cache_ubinder x);
- classify_function = (fun x -> Substitute x);
- subst_function = subst_ubinder;
- discharge_function = discharge_ubinder;
- rebuild_function = (fun x -> x); }
-
-let register_universe_binders ref ubinders =
- let open Names in
- (* Add the polymorphic (section) universes *)
- let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
- let qid = Nametab.shortest_qualid_of_universe lvl in
- let level = Level.make (fst lvl) (snd lvl) in
- if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
- else ubinders)
- !universe_map ubinders
- in
- if not (Id.Map.is_empty ubinders)
- then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-
-type univ_name_list = Misctypes.lname list
-
-let universe_binders_with_opt_names ref levels = function
- | None -> universe_binders_of_global ref
- | Some udecl ->
- if Int.equal(List.length levels) (List.length udecl)
- then
- List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
- | Anonymous -> acc
- | Name na -> Names.Id.Map.add na lvl acc)
- empty_binders udecl levels
- else
- CErrors.user_err ~hdr:"universe_binders_with_opt_names"
- Pp.(str "Universe instance should have length " ++ int (List.length levels))
(* To disallow minimization to Set *)
@@ -917,6 +821,9 @@ let minimize_univ_variables ctx us algs left right cstrs =
else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs)
us (ctx, us, algs, lbounds, cstrs)
+module UPairs = OrderedType.UnorderedPair(Univ.Level)
+module UPairSet = Set.Make (UPairs)
+
let normalize_context_set g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
(** Keep the Prop/Set <= i constraints separate for minimization *)
@@ -1111,3 +1018,21 @@ let solve_constraints_system levels level_bounds level_min =
done;
done;
v
+
+(** Deprecated *)
+type universe_binders = UnivNames.universe_binders
+type univ_name_list = UnivNames.univ_name_list
+
+let pr_with_global_universes = UnivNames.pr_with_global_universes
+let reference_of_level = UnivNames.reference_of_level
+
+let add_global_universe = UnivNames.add_global_universe
+
+let is_polymorphic = UnivNames.is_polymorphic
+
+let empty_binders = UnivNames.empty_binders
+
+let register_universe_binders = UnivNames.register_universe_binders
+let universe_binders_of_global = UnivNames.universe_binders_of_global
+
+let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
diff --git a/engine/universes.mli b/engine/universes.mli
index 46d65f257..aaf295c1d 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -19,35 +19,6 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
(** Universes *)
-val pr_with_global_universes : Level.t -> Pp.t
-val reference_of_level : Level.t -> Libnames.reference
-
-(** Global universe information outside the kernel, to handle
- polymorphic universes in sections that have to be discharged. *)
-val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
-
-val is_polymorphic : Level.t -> bool
-
-(** Local universe name <-> level mapping *)
-
-type universe_binders = Univ.Level.t Names.Id.Map.t
-
-val empty_binders : universe_binders
-
-val register_universe_binders : GlobRef.t -> universe_binders -> unit
-val universe_binders_of_global : GlobRef.t -> universe_binders
-
-type univ_name_list = Misctypes.lname list
-
-(** [universe_binders_with_opt_names ref u l]
-
- If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
- May error if the lengths mismatch.
-
- Otherwise return [universe_binders_of_global ref]. *)
-val universe_binders_with_opt_names : Names.GlobRef.t ->
- Univ.Level.t list -> univ_name_list option -> universe_binders
-
(** The global universe counter *)
type universe_id = DirPath.t * int
@@ -226,3 +197,41 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
Universe.t array
+
+(** *********************************** Deprecated *)
+[@@@ocaml.warning "-3"]
+val set_minimization : bool ref
+[@@ocaml.deprecated "Becoming internal."]
+val is_set_minimization : unit -> bool
+[@@ocaml.deprecated "Becoming internal."]
+
+(** ****** Deprecated: moved to [UnivNames] *)
+
+val pr_with_global_universes : Level.t -> Pp.t
+[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"]
+val reference_of_level : Level.t -> Libnames.reference
+[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"]
+
+val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit
+[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"]
+
+val is_polymorphic : Level.t -> bool
+[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"]
+
+type universe_binders = UnivNames.universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders]"]
+
+val empty_binders : universe_binders
+[@@ocaml.deprecated "Use [UnivNames.empty_binders]"]
+
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
+
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
+
+val universe_binders_with_opt_names : Globnames.global_reference ->
+ Univ.Level.t list -> univ_name_list option -> universe_binders
+[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
diff --git a/interp/declare.ml b/interp/declare.ml
index c55a6c69b..34bf5c8a2 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -487,7 +487,7 @@ let add_universe src (dp, i) =
Option.iter (fun poly ->
let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
Global.push_context_set poly ctx;
- Universes.add_global_universe level poly;
+ UnivNames.add_global_universe level poly;
if poly then Lib.add_section_context ctx)
optpoly
@@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj =
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
- Universes.register_universe_binders gr pl
+ UnivNames.register_universe_binders gr pl
else
let l = match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
@@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj =
let do_constraint poly l =
let u_of_id x =
let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
- Universes.is_polymorphic level, level
+ UnivNames.is_polymorphic level, level
in
let in_section = Lib.sections_are_opened () in
let () =
diff --git a/interp/declare.mli b/interp/declare.mli
index f8cffbb1e..0d795c497 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) ->
val exists_name : Id.t -> bool
(** Global universe contexts, names and constraints *)
-val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 3a49d6cf8..67a526bc1 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -32,8 +32,8 @@ type goal_reference =
| NthGoal of int
| GoalId of Id.t
-type univ_name_list = Universes.univ_name_list
-[@@ocaml.deprecated "Use [Universes.univ_name_list]"]
+type univ_name_list = UnivNames.univ_name_list
+[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
type printable =
| PrintTables
@@ -49,7 +49,7 @@ type printable =
| PrintMLLoadPath
| PrintMLModules
| PrintDebugGC
- | PrintName of reference or_by_notation * Universes.univ_name_list option
+ | PrintName of reference or_by_notation * UnivNames.univ_name_list option
| PrintGraph
| PrintClasses
| PrintTypeClasses
@@ -65,7 +65,7 @@ type printable =
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
- | PrintAbout of reference or_by_notation * Universes.univ_name_list option * Goal_select.t option
+ | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
| PrintImplicit of reference or_by_notation
| PrintAssumptions of bool * bool * reference or_by_notation
| PrintStrategy of reference or_by_notation option
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 185b1648c..d036fec21 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,8 +35,8 @@ open Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
type object_pr = {
- print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
- print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
@@ -93,7 +93,7 @@ let print_ref reduce ref udecl =
let inst = Univ.AUContext.instance univs in
let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
let env = Global.env () in
- let bl = Universes.universe_binders_with_opt_names ref
+ let bl = UnivNames.universe_binders_with_opt_names ref
(Array.to_list (Univ.Instance.to_array inst)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let inst =
@@ -594,7 +594,7 @@ let print_constant with_values sep sp udecl =
in
let ctx =
UState.of_binders
- (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+ (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
in
let env = Global.env () and sigma = Evd.from_ctx ctx in
let pr_ltype = pr_ltype_env env sigma in
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 2f2dcd563..50042d6c5 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -34,10 +34,10 @@ val print_eval :
Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
val print_name : env -> Evd.evar_map -> reference or_by_notation ->
- Universes.univ_name_list option -> Pp.t
+ UnivNames.univ_name_list option -> Pp.t
val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
val print_about : env -> Evd.evar_map -> reference or_by_notation ->
- Universes.univ_name_list option -> Pp.t
+ UnivNames.univ_name_list option -> Pp.t
val print_impargs : reference or_by_notation -> Pp.t
(** Pretty-printing functions for classes and coercions *)
@@ -84,8 +84,8 @@ val print_located_module : reference -> Pp.t
val print_located_other : string -> reference -> Pp.t
type object_pr = {
- print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t;
- print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
+ print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
+ print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
print_section_variable : env -> Evd.evar_map -> variable -> Pp.t;
print_syntactic_def : env -> KerName.t -> Pp.t;
print_module : bool -> ModPath.t -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index edcce874d..77466605a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_global = pr_global_env Id.Set.empty
let pr_puniverses f env (c,u) =
f env c ++
(if !Constrextern.print_universes then
- str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
else mt ())
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e076c10f3..3c805b327 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -140,7 +140,7 @@ let print_mutual_inductive env mind mib udecl =
(AUContext.instance (Declareops.inductive_polymorphic_context mib)))
else []
in
- let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+ let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
Printer.pr_cumulative
@@ -183,7 +183,7 @@ let print_record env mind mib udecl =
let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
- let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+ let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
(Array.to_list (Univ.Instance.to_array u)) udecl in
let sigma = Evd.from_ctx (UState.of_binders bl) in
let keyword =
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0b0b0a35..48ba866cc 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -15,6 +15,6 @@ val printable_body : DirPath.t -> bool
val pr_mutual_inductive_body : Environ.env ->
MutInd.t -> Declarations.mutual_inductive_body ->
- Universes.univ_name_list option -> Pp.t
+ UnivNames.univ_name_list option -> Pp.t
val print_module : bool -> ModPath.t -> Pp.t
val print_modtype : ModPath.t -> Pp.t
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1ac597695..61ce5d6c4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -423,13 +423,13 @@ let context poly l =
let decl = (Discharge, poly, Definitional) in
let nstatus = match b with
| None ->
- pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
+ pi3 (ComAssumption.declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
Declaremods.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
let hook = Lemmas.mk_hook (fun _ gr -> gr) in
- let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
+ let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 2f2c7c4e2..56932360a 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -30,6 +30,6 @@ val do_assumptions : locality * polymorphic * assumption_object_kind ->
nor in a module type and meant to be instantiated. *)
val declare_assumption : coercion_flag -> assumption_kind ->
types in_constant_universes_entry ->
- Universes.universe_binders -> Impargs.manual_implicits ->
+ UnivNames.universe_binders -> Impargs.manual_implicits ->
bool (** implicit *) -> Declaremods.inline -> variable CAst.t ->
GlobRef.t * Univ.Instance.t * bool
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 833935724..7ae8e8f71 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -37,7 +37,7 @@ type one_inductive_impls =
Impargs.manual_implicits list (** for constrs *)
val declare_mutual_inductive_with_eliminations :
- mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
+ mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
(** Exported for Funind *)
@@ -64,4 +64,4 @@ val extract_mutual_inductive_declaration_components :
val interp_mutual_inductive :
structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> Declarations.recursivity_kind ->
- mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
+ mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 349fc562b..f41e0fc44 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -212,7 +212,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
- let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in
+ let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 12973f51b..c5e704a5e 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,11 +14,11 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition : Id.t -> definition_kind ->
- Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+ Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
GlobRef.t Lemmas.declaration_hook -> GlobRef.t
val declare_fix : ?opaque:bool -> definition_kind ->
- Universes.universe_binders -> Entries.constant_universes_entry ->
+ UnivNames.universe_binders -> Entries.constant_universes_entry ->
Id.t -> Safe_typing.private_constants Entries.proof_output ->
Constr.types -> Impargs.manual_implicits ->
GlobRef.t
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f9167f969..f68dcae26 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -55,7 +55,7 @@ let process_vernac_interp_error exn = match fst exn with
let msg =
if !Constrextern.print_universes then
str "." ++ spc() ++
- Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i
else
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index acb461cac..3c4fcf714 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -197,7 +197,7 @@ let rec pr_disjunction pr = function
let pr_puniverses f env (c,u) =
f env c ++
(if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
- str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
else mt())
let explain_elim_arity env sigma ind sorts c pj okinds =
@@ -314,7 +314,7 @@ let explain_unification_error env sigma p1 p2 = function
| UnifUnivInconsistency p ->
if !Constrextern.print_universes then
[str "universe inconsistency: " ++
- Univ.explain_universe_inconsistency Universes.pr_with_global_universes p]
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p]
else
[str "universe inconsistency"]
| CannotSolveConstraint ((pb,env,t,u),e) ->
@@ -886,7 +886,7 @@ let explain_not_match_error = function
str"polymorphic universe instances do not match"
| IncompatibleUniverses incon ->
str"the universe constraints are inconsistent: " ++
- Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon
+ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
| IncompatiblePolymorphism (env, t1, t2) ->
str "conversion of polymorphic values generates additional constraints: " ++
quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ae1065ef5..6de8539d4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -555,7 +555,7 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.const_univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
diff --git a/vernac/record.ml b/vernac/record.ml
index b89c0060d..421997dce 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -316,7 +316,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
let kn = destConstRef gr in
Declare.definition_message fid;
- Universes.register_universe_binders gr ubinders;
+ UnivNames.register_universe_binders gr ubinders;
kn, mkProj (Projection.make kn false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
@@ -352,7 +352,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
applist (mkConstU (kn,u),proj_args)
in
Declare.definition_message fid;
- Universes.register_universe_binders (ConstRef kn) ubinders;
+ UnivNames.register_universe_binders (ConstRef kn) ubinders;
kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
@@ -465,9 +465,9 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
in
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref [paramimpls];
- Universes.register_universe_binders cref ubinders;
+ UnivNames.register_universe_binders cref ubinders;
Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
- Universes.register_universe_binders (ConstRef proj_cst) ubinders;
+ UnivNames.register_universe_binders (ConstRef proj_cst) ubinders;
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
diff --git a/vernac/record.mli b/vernac/record.mli
index 308c9e9b9..b2c039f0b 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,7 @@ val declare_projections :
?kind:Decl_kinds.definition_object_kind ->
Id.t ->
bool list ->
- Universes.universe_binders ->
+ UnivNames.universe_binders ->
Impargs.manual_implicits list ->
Context.Rel.t ->
(Name.t * bool) list * Constant.t option list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f0e41d27c..7ccc411db 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1741,7 +1741,7 @@ let vernac_print ~atts env sigma =
else str"There may remain asynchronous universe constraints"
in
begin match dst with
- | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining
+ | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining
| Some s -> dump_universes_gen univ s
end
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 11:32:20 +0000