diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 11:25:29 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-28 11:25:29 +0200 |
| commit | 66a68a4329ce199f25184ba8b2d98b4679e7ddae (patch) | |
| tree | ce90c93341c58e82813da8b1a567ce6a3f3ed424 /vernac/lemmas.mli | |
| parent | 0a255f51809e8d29a7239bfbd9fe57a8b2b41705 (diff) | |
| parent | 2ddc9d12bd4616f10245c40bc0c87ae548911809 (diff) | |
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of let-ins
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 681413a29..d06b8fd14 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 : |