From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 17:58:08 +0200 Subject: Split off Universes functions dealing with names. This API is a bit strange, I expect it will change at some point. --- dev/top_printers.ml | 2 +- engine/engine.mllib | 1 + engine/evd.mli | 4 +- engine/termops.ml | 2 +- engine/uState.ml | 4 +- engine/uState.mli | 4 +- engine/univNames.ml | 105 ++++++++++++++++++++++++++++++++++++++ engine/univNames.mli | 41 +++++++++++++++ engine/universes.ml | 117 ++++++++----------------------------------- engine/universes.mli | 67 ++++++++++++++----------- interp/declare.ml | 6 +-- interp/declare.mli | 2 +- pretyping/vernacexpr.ml | 8 +-- printing/prettyp.ml | 8 +-- printing/prettyp.mli | 8 +-- printing/printer.ml | 2 +- printing/printmod.ml | 4 +- printing/printmod.mli | 2 +- vernac/classes.ml | 4 +- vernac/comAssumption.mli | 2 +- vernac/comInductive.mli | 4 +- vernac/comProgramFixpoint.ml | 2 +- vernac/declareDef.mli | 4 +- vernac/explainErr.ml | 2 +- vernac/himsg.ml | 6 +-- vernac/obligations.ml | 2 +- vernac/record.ml | 8 +-- vernac/record.mli | 2 +- vernac/vernacentries.ml | 2 +- 29 files changed, 253 insertions(+), 172 deletions(-) create mode 100644 engine/univNames.ml create mode 100644 engine/univNames.mli 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 *) +(* + 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 *) +(* 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) -- cgit v1.2.3