diff options
| author | corbinea | 2003-03-28 13:30:24 +0000 |
|---|---|---|
| committer | corbinea | 2003-03-28 13:30:24 +0000 |
| commit | 49db22be8b253900362f210ebd800ba1d326e589 (patch) | |
| tree | d7e9a593bed9bc4301710038ca27870a6f5442ca | |
| parent | 3d29ae897bd291994a81df69096be3dfee17c418 (diff) | |
Fixed Relative names not,iff in Camlp4 quotation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/newtauto.ml4 | 9 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 21 |
2 files changed, 14 insertions, 16 deletions
diff --git a/tactics/newtauto.ml4 b/tactics/newtauto.ml4 index f378bbe803..04ecc36fa2 100644 --- a/tactics/newtauto.ml4 +++ b/tactics/newtauto.ml4 @@ -56,10 +56,7 @@ let isrec ind= let (mib,mip) = Global.lookup_inductive ind in Inductiveops.mis_is_recursive (ind,mib,mip) -let simplif=interp - <:tactic<Repeat (Match Context With - |[|- ?]->Progress Unfold not iff - |[H:?|- ?]->Progress Unfold not iff in H)>> +let simplif=Tauto.reduction_not_iff let rule_axiom=assumption @@ -207,9 +204,7 @@ let q_elim tac= let vtac=Tacexpr.TacArg (valueIn (VTactic tac)) in interp <:tactic< Match Context With - [x:?1|-(? ?1 ?)]-> - Exists x;$vtac - |[x:?1;H:?1->?|-?]-> + [x:?1;H:?1->?|-?]-> Generalize (H x);Clear H;$vtac>> let rec lfo n= diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 2a0a01f43d..36ee7e18a6 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -52,12 +52,12 @@ let not_dep_intros ist = Repeat Match Context With | [|- ?1 -> ?2 ] -> Intro -| [|- (iff ? ?)] -> Unfold iff -| [|- (not ?)] -> Unfold not -| [ H:(iff ? ?)|- ?] -> Unfold iff in H -| [ H:(not ?)|-?] -> Unfold not in H -| [ H:(iff ? ?)->?|- ?] -> Unfold iff in H -| [ H:(not ?)->?|-?] -> Unfold not in H >> +| [|- (Coq.Init.Logic.iff ? ?)] -> Unfold Coq.Init.Logic.iff +| [|- (Coq.Init.Logic.not ?)] -> Unfold Coq.Init.Logic.not +| [ H:(Coq.Init.Logic.iff ? ?)|- ?] -> Unfold Coq.Init.Logic.iff in H +| [ H:(Coq.Init.Logic.not ?)|-?] -> Unfold Coq.Init.Logic.not in H +| [ H:(Coq.Init.Logic.iff ? ?)->?|- ?] -> Unfold Coq.Init.Logic.iff in H +| [ H:(Coq.Init.Logic.not ?)->?|-?] -> Unfold Coq.Init.Logic.not in H >> let axioms ist = let t_is_unit = tacticIn is_unit @@ -136,9 +136,12 @@ let rec tauto_intuit t_reduce t_solver ist = ) >> let reduction_not_iff=interp - <:tactic<Repeat (Match Context With - |[|- ?]->Progress Unfold not iff - |[H:?|- ?]->Progress Unfold not iff in H)>> + <:tactic<Repeat + (Match Context With + |[|- ?]-> + Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff + |[H:?|- ?]-> + Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff in H)>> let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff)) |