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/Lra.v b/plugins/micromega/Lra.v
index 4d9cf22dd..5b97d8ed3 100644
--- a/plugins/micromega/Lra.v
+++ b/plugins/micromega/Lra.v
@@ -26,23 +26,20 @@ Ltac rchange :=
   apply (RTautoChecker_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 real arithmetic *)
-Ltac lra := unfold Rdiv in * ;   lra_R ; rchecker.
+Ltac lra := unfold Rdiv in * ;   lra_R  rchecker.
 
 (** Here, nra stands for non-linear real arithmetic *)
-Ltac nra := unfold Rdiv in * ; xnra ; rchecker.
+Ltac nra := unfold Rdiv in * ; xnra  rchecker.
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | R =>
-    (sos_R || psatz_R 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_R rchecker) || (psatz_R d rchecker)
   | _ => fail "Unsupported domain"
  end in tac.