diff options
Diffstat (limited to 'plugins/micromega/Lqa.v')
| -rw-r--r-- | plugins/micromega/Lqa.v | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v index e3414b849..acd2751a0 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -25,23 +25,20 @@ Ltac rchange := apply (QTautoChecker_sound __ff __wit). Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. -Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). +Ltac rchecker_abstract := rchange ; vm_cast_no_check (eq_refl true). -Ltac rchecker := (rchecker_abstract || rchecker_no_abstract). +Ltac rchecker := rchecker_no_abstract. (** Here, lra stands for linear rational arithmetic *) -Ltac lra := lra_Q ; rchecker. +Ltac lra := lra_Q rchecker. (** Here, nra stands for non-linear rational arithmetic *) -Ltac nra := xnqa ; rchecker. +Ltac nra := xnqa rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with | Q => - (sos_Q || psatz_Q d) ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try rchecker + ((sos_Q rchecker) || (psatz_Q d rchecker)) | _ => fail "Unsupported domain" end in tac. |