aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
diff options
context:
space:
mode:
authorGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-28 08:36:26 +0000
committerGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-28 08:36:26 +0000
commit6c7328c96b9ca6921db1569ee085bee16df48e91 (patch)
treea381e30035f632ce57f4feeb9f271185f9d7329f /plugins/micromega
parentaabccf49938d5727cc1c7a53882ce1f5108bbed5 (diff)
improved tactic names
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14242 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/Psatz.v13
1 files changed, 4 insertions, 9 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 4fef3d790..88d0332dc 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -78,21 +78,16 @@ Ltac psatzl dom :=
Ltac lra :=
- unfold Rdiv in * ;
- psatzl_R ;
- try (intros __wit __varmap __ff ;
- change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
- apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
-
+ first [ psatzl R | psatzl Q ].
Ltac lia :=
- cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ; xlia ;
+ (*cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ;*) xlia ;
intros __wit __varmap __ff ;
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
-Ltac nlia :=
- cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ; xnlia ;
+Ltac nia :=
+ xnlia ;
intros __wit __varmap __ff ;
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.