diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /library/declare.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
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 |