diff options
| author | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
| commit | 424c1973e96dfbf3b2e3245d735853ffa9600373 (patch) | |
| tree | af087fa873c709e0066c8f6d81898f3aeae59b21 /plugins/micromega/Lqa.v | |
| parent | 943fdd3277909f5229d95eb2e486944b0258648c (diff) | |
| parent | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (diff) | |
Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and #9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
Diffstat (limited to 'plugins/micromega/Lqa.v')
| -rw-r--r-- | plugins/micromega/Lqa.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v index caaec541eb..f3cd24be8a 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -18,12 +18,13 @@ Require Import QMicromega. Require Import QArith. Require Import RingMicromega. Require Import VarMap. +Require Import DeclConstant. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac rchange := intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit). Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. |