diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-18 21:38:19 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-18 21:38:19 +0000 |
| commit | 9d66e886d4c8dcf8b6cb44923d06913161e2cf5c (patch) | |
| tree | d882fbf132a771036068df46a2e57df44eed89be /plugins/micromega/Psatz.v | |
| parent | 95c80b62371bf66da847a5a42b7e8ca2bcef12b5 (diff) | |
cbv delta - [...] before calling lia
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14140 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 39c98bc5d..84ce85f29 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -76,13 +76,13 @@ Ltac psatzl dom := end in tac. Ltac lia := - 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 := - xnlia ; + cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ; xnlia ; intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. |