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 /vernac/comDefinition.mli | |
| 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 'vernac/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 6c6da8952e..7902b0ef09 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,8 +15,20 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool - -> ?hook:DeclareDef.Hook.t + : ?hook:DeclareDef.Hook.t + -> name:Id.t + -> scope:DeclareDef.locality + -> poly:bool + -> kind:Decls.definition_object_kind + -> universe_decl_expr option + -> local_binder_expr list + -> red_expr option + -> constr_expr + -> constr_expr option + -> unit + +val do_definition_program + : ?hook:DeclareDef.Hook.t -> name:Id.t -> scope:DeclareDef.locality -> poly:bool |