diff options
| author | Matej Kosik | 2016-07-29 16:14:52 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-07-29 16:14:52 +0200 |
| commit | 81c19bdd631fa72afa0cac5c8b915d836e0646df (patch) | |
| tree | 98bc7e3154217fec508bb0477fe98f1a786651e0 /library | |
| parent | e3faeb71580f85394042028499bbc9573efc23cb (diff) | |
COMMENT: moving misplaced comment where it belongs
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.mli | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/library/declare.mli b/library/declare.mli index 8dd24d2780..7824506da0 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 |