diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 02:47:01 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:06:35 -0400 |
| commit | 8129fb2abce6ba2e5ddd1f384618bb2fb8f817b5 (patch) | |
| tree | 982db7b802ed407db6ac3bd967cb610b6b48f562 /vernac/declareDef.mli | |
| parent | a15e584571a4e153e98a11c93d12759c45ea2dcd (diff) | |
[proof] [mutual] Factorize mutual per-entry information
We move `Recthm` to `DeclareDef` so it is shared by interactive and
direct fixpoint declaration.
This is the last step before unifying both paths.
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 05a38c039d..995aa0ceff 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -59,6 +59,19 @@ val declare_assumption -> Entries.parameter_entry -> GlobRef.t +module Recthm : sig + type t = + { name : Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + val declare_mutually_recursive : opaque:bool -> scope:locality @@ -70,9 +83,7 @@ val declare_mutually_recursive -> rec_declaration:Constr.rec_declaration -> possible_indexes:int list list option -> restrict_ucontext:bool - -> Names.variable list - -> Constr.types list - -> Impargs.manual_implicits list + -> Recthm.t list -> Names.GlobRef.t list val prepare_definition |