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/comDefinition.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/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 7902b0ef09..337da22018 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -39,19 +39,3 @@ val do_definition_program -> constr_expr -> constr_expr option -> unit - -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Not used anywhere. *) -val interp_definition - : program_mode:bool - -> universe_decl_expr option - -> local_binder_expr list - -> poly:bool - -> red_expr option - -> constr_expr - -> constr_expr option - -> Evd.side_effects Declare.proof_entry * - Evd.evar_map * UState.universe_decl * Impargs.manual_implicits |