diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-01 19:27:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-03 16:51:09 +0200 |
| commit | 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 (patch) | |
| tree | d64a667a3a5ec7c22705739d6b25b36bad24ad7c /ltac/tacinterp.ml | |
| parent | 9d60ddc84e95a030913fc4b3db705f3ec894fdb2 (diff) | |
Removing "double induction" from the tactic AST.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index fcc29a830..f6f988ee2 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1822,12 +1822,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Sigma.Unsafe.of_pair (tac, sigma) end } - | TacDoubleInduction (h1,h2) -> - let h1 = interp_quantified_hypothesis ist h1 in - let h2 = interp_quantified_hypothesis ist h2 in - name_atomic - (TacDoubleInduction (h1,h2)) - (Elim.h_double_induction h1 h2) (* Context management *) | TacRename l -> Proofview.Goal.enter { enter = begin fun gl -> |