diff options
| author | Gaëtan Gilbert | 2020-08-31 12:54:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-31 12:56:13 +0200 |
| commit | e5890700b4574ee9207b2daf6ec95707b9290275 (patch) | |
| tree | 1cae11e386b200d0d93bbc3802bff27b954019ab | |
| parent | 4c3064c6e679cfbe4ce13a76b50a17bcfffe4d71 (diff) | |
Fix mangle names issue in induction
Fix #12944
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12944.v | 12 |
2 files changed, 13 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 00bd56d8ba..28e841d4ae 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3317,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> - let id' = next_ident_away (add_prefix "IH" id) avoid in + let id' = new_fresh_id avoid (add_prefix "IH" id) gl in (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v new file mode 100644 index 0000000000..d6720d9906 --- /dev/null +++ b/test-suite/bugs/closed/bug_12944.v @@ -0,0 +1,12 @@ + +Inductive vector A : nat -> Type := + |nil : vector A 0 + |cons : forall (h:A) (n:nat), vector A n -> vector A (S n). + +Global Set Mangle Names. + +Lemma vlookup_middle {A n} (v : vector A n) : True. +Proof. + induction v as [|?? IHv]. + all:exact I. +Qed. |