diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2014-08-01 18:42:26 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2014-08-01 18:42:26 +0200 |
| commit | fb50696d492027744c3c9044fd863f93e0a1605c (patch) | |
| tree | 69003e4485d5a3f7cbebffc54328ac3f0a2426c5 /plugins/micromega/Lia.v | |
| parent | a8d440fcb2a5f5768874012e72c3e092eb82eff1 (diff) | |
micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)
* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
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: *) |