diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 06:54:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-20 11:21:30 +0200 |
| commit | ec8523065abfb68aff9bd3664869224419885385 (patch) | |
| tree | 0d5d3397e52704baefbb273807a61a3cc81f6340 /vernac/declareDef.mli | |
| parent | 21f8312738f324d1c55e4ed7c451b642c9da70e6 (diff) | |
[vernac] Remove forward hooks from Obligations.
This was (once again) a spurious inter-dependency, that we solve by
introducing a new module with the proper functionality. This helps in
cleaning up the code. Note that no code was changed, other than
removing the setting of the references.
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli new file mode 100644 index 000000000..5dea0ba27 --- /dev/null +++ b/vernac/declareDef.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Decl_kinds +open Names + +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 -> + Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference + +val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> + Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference |