diff options
Diffstat (limited to 'plugins/micromega/Lia.v')
| -rw-r--r-- | plugins/micromega/Lia.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index add394539..aaa42d1f9 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -24,19 +24,19 @@ Ltac preprocess := Ltac lia := preprocess; - (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ; + xlia ; abstract ( intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). Ltac nia := preprocess; xnlia ; abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). (* Local Variables: *) |