diff options
Diffstat (limited to 'tactics/tauto.ml4')
-rw-r--r-- | tactics/tauto.ml4 | 42 |
1 files changed, 6 insertions, 36 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index e62b50bd0..3c65fe159 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -10,8 +10,6 @@ (*i $Id$ i*) -open Ast -open Coqast open Hipattern open Names open Libnames @@ -171,39 +169,11 @@ let tauto g = let default_intuition_tac = interp <:tactic< auto with * >> -let q_elim tac= - <:tactic< - match goal with - x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac - end >> - -let rec lfo n gl= - if n=0 then (tclFAIL 0 "LinearIntuition failed" gl) else - let p=if n<0 then n else (n-1) in - let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic(dummy_loc,lfo p)))) in - intuition_gen (interp lfo_rec) gl - -let lfo_wrap n gl= - try lfo n gl - with - Refiner.FailError _ | UserError _ -> - errorlabstrm "LinearIntuition" [< str "LinearIntuition failed." >] - -TACTIC EXTEND Tauto -| [ "Tauto" ] -> [ tauto ] -END -(* Obsolete sinve V8.0 -TACTIC EXTEND TSimplif -| [ "Simplif" ] -> [ simplif_gen ] +TACTIC EXTEND tauto +| [ "tauto" ] -> [ tauto ] END -*) -TACTIC EXTEND Intuition -| [ "Intuition" ] -> [ intuition_gen default_intuition_tac ] -| [ "Intuition" tactic(t) ] -> [ intuition_gen (snd t) ] -END -(* Obsolete since V8.0 -TACTIC EXTEND LinearIntuition -| [ "LinearIntuition" ] -> [ lfo_wrap (-1)] -| [ "LinearIntuition" integer(n)] -> [ lfo_wrap n] + +TACTIC EXTEND intuition +| [ "intuition" ] -> [ intuition_gen default_intuition_tac ] +| [ "intuition" tactic(t) ] -> [ intuition_gen (snd t) ] END -*) |