diff options
| author | Pierre-Marie Pédrot | 2016-04-01 19:27:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-03 16:51:09 +0200 |
| commit | 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 (patch) | |
| tree | d64a667a3a5ec7c22705739d6b25b36bad24ad7c /ltac | |
| parent | 9d60ddc84e95a030913fc4b3db705f3ec894fdb2 (diff) | |
Removing "double induction" from the tactic AST.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 7 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 4 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 6 | ||||
| -rw-r--r-- | ltac/tacsubst.ml | 1 |
4 files changed, 7 insertions, 11 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index ce28eacc09..63b5463c49 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -222,6 +222,13 @@ TACTIC EXTEND simple_destruct [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ] END +(** Double induction *) + +TACTIC EXTEND double_induction + [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + [ Elim.h_double_induction h1 h2 ] +END + (* Admit *) TACTIC EXTEND admit diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 3744449e97..0f827755a6 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -520,10 +520,6 @@ let rec intern_atomic lf ist x = Option.map (intern_or_and_intro_pattern_loc lf ist) ipats), Option.map (clause_app (intern_hyp_location ist)) cls)) l, Option.map (intern_constr_with_bindings ist) el)) - | TacDoubleInduction (h1,h2) -> - let h1 = intern_quantified_hypothesis ist h1 in - let h2 = intern_quantified_hypothesis ist h2 in - TacDoubleInduction (h1,h2) (* Context management *) | TacRename l -> TacRename (List.map (fun (id1,id2) -> diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index fcc29a8302..f6f988ee23 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 -> diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 3f504b7f37..71dd718e87 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -162,7 +162,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with subst_induction_arg subst c, ids, cls) l in let el' = Option.map (subst_glob_with_bindings subst) el in TacInductionDestruct (isrec,ev,(l',el')) - | TacDoubleInduction (h1,h2) as x -> x (* Context management *) | TacRename l as x -> x |