From 2ddc9d12bd4616f10245c40bc0c87ae548911809 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Apr 2017 19:13:58 +0200 Subject: Fixing #5420 as well as many related bugs due to miscounting let-ins. - Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins. --- vernac/lemmas.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/lemmas.mli') 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 : -- cgit v1.2.3