diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/library/declare.mli b/library/declare.mli index 8dd24d27..f70d594d 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -34,14 +34,6 @@ val declare_variable : variable -> variable_declaration -> object_name type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent - - *) type internal_flag = | UserAutomaticRequest | InternalTacticRequest @@ -53,6 +45,12 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry +(** [declare_constant id cd] declares a global declaration + (constant/parameter) with name [id] in the current section; it returns + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent *) val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant @@ -89,7 +87,11 @@ val exists_name : Id.t -> bool -(** Global universe names and constraints *) +(** Global universe contexts, names and constraints *) + +val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit +val do_constraint : polymorphic -> + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit |