diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 02:27:54 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 (patch) | |
| tree | 020c8aded6b220f4bc022555673e0737445e9107 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 76115e703751cfde99d7e86be9eea8fb32398e8a (diff) | |
[ComDefinition] Split program from regular declarations
Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly
more complicated in the Program case; in particular, it includes
checking the existential variables, and elaborating a list of entries
from the holes.
Indeed, in the `Program` case we cannot use
`DeclareDef.prepare_definition` while keeping a good level of
abstraction, so we should introduce a `prepare_obligation` function.
This PR is in preparation for that.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions