micromega : more robust generation of proof terms

- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
  (This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)

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.