diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 08:36:26 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 08:36:26 +0000 |
| commit | 6c7328c96b9ca6921db1569ee085bee16df48e91 (patch) | |
| tree | a381e30035f632ce57f4feeb9f271185f9d7329f /plugins/micromega | |
| parent | aabccf49938d5727cc1c7a53882ce1f5108bbed5 (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.v | 13 |
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. |