diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 44 |
1 files changed, 7 insertions, 37 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 553acc91..c91038fc 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,10 +8,8 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4,v 1.62.2.1 2004/07/16 19:30:55 herbelin Exp $ i*) +(*i $Id: tauto.ml4 7732 2005-12-26 13:51:24Z herbelin $ 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 -*) |