diff options
| author | Pierre-Marie Pédrot | 2020-08-29 18:25:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-31 10:21:35 +0200 |
| commit | bb09af9e9cfa32f89cb5538a6e51af5dae6cc467 (patch) | |
| tree | 6bfae708f5448adfac66f7cfa8c3cc6070e9cae1 /tactics/tactics.ml | |
| parent | 9c9bf136430213eacec8e32ad4909cf501141a48 (diff) | |
Move elim-specific code from Tacticals to Elim.
No reason to have them there.
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 eb7b7e363f..e2d60dfabd 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) |