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 /doc/plugin_tutorial/tuto1 | |
| 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 'doc/plugin_tutorial/tuto1')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 2fdca15552..3b906324f4 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,5 +1,5 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false + let sigma, ce = DeclareDef.prepare_definition ~opaque ~poly sigma ~udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubind = Evd.universe_binders sigma in |