diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3b2481bc69..5f7e35d205 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4397,7 +4397,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in - let names = compute_induction_names branchletsigns names in + let names = compute_induction_names true branchletsigns names in Array.iter (check_name_unicity env toclear []) names; let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) |