diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/classes.ml | 4 | ||||
-rw-r--r-- | vernac/comAssumption.mli | 2 | ||||
-rw-r--r-- | vernac/comInductive.mli | 4 | ||||
-rw-r--r-- | vernac/comProgramFixpoint.ml | 2 | ||||
-rw-r--r-- | vernac/declareDef.mli | 4 | ||||
-rw-r--r-- | vernac/explainErr.ml | 2 | ||||
-rw-r--r-- | vernac/himsg.ml | 6 | ||||
-rw-r--r-- | vernac/obligations.ml | 2 | ||||
-rw-r--r-- | vernac/record.ml | 8 | ||||
-rw-r--r-- | vernac/record.mli | 2 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 2 |
11 files changed, 19 insertions, 19 deletions
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) |