diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 03:07:42 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 56ffe818ab7706a82d79b538fdf3af8b23d95f40 (patch) | |
| tree | f984d2ea14406547b031b41a3a1bc48d9989d533 /vernac/declareDef.mli | |
| parent | 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 (diff) | |
[declare] [obligations] Refactor preparation of obligation entry
Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.
This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:
- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index e999027b44..27d9460382 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -89,8 +89,7 @@ val declare_mutually_recursive -> Names.GlobRef.t list val prepare_definition - : allow_evars:bool - -> ?opaque:bool + : ?opaque:bool -> ?inline:bool -> poly:bool -> udecl:UState.universe_decl @@ -99,6 +98,17 @@ val prepare_definition -> Evd.evar_map -> Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_obligation + : ?opaque:bool + -> ?inline:bool + -> name:Id.t + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info + val prepare_parameter : allow_evars:bool -> poly:bool |