diff options
| -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. |