diff options
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 39c089be9..6b45ed933 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -41,8 +41,8 @@ val start_proof_com : val start_proof_with_initialization : goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t * universe_binders option) * - (types * (Name.t list * Impargs.manual_explicitation list))) list + ((Id.t (* name of thm *) * universe_binders option) * + (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val universe_proof_terminator : |