diff options
author | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-29 16:58:47 +0000 |
---|---|---|
committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-29 16:58:47 +0000 |
commit | e20e6b3b9e4148f62c94bfb467817feb2b6a4583 (patch) | |
tree | bbb4359c0799c45902314b4a53aee9882d3590f1 /plugins/micromega | |
parent | e97cd3c0cab1eb022b15d65bb33483055ce4cc28 (diff) |
update of Micromega doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega')
-rw-r--r-- | plugins/micromega/Psatz.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 88d0332dc..7f6cf79be 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -81,12 +81,14 @@ Ltac lra := first [ psatzl R | psatzl Q ]. Ltac lia := + zify ; unfold Zsucc in * ; (*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 nia := + zify ; unfold Zsucc in * ; xnlia ; intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; |