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, 3 insertions, 9 deletions

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index c81c025a5..8acf0ff88 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -35,16 +35,10 @@ Ltac nia := Lia.nia.
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z =>
-    (sos_Z || psatz_Z d) ; Lia.zchecker
+    (sos_Z Lia.zchecker) || (psatz_Z d  Lia.zchecker)
   | 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 Lra.rchecker
-  | 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  Lqa.rchecker
+    (sos_R Lra.rchecker) || (psatz_R d Lra.rchecker)
+  | Q => (sos_Q Lqa.rchecker) || (psatz_Q d Lqa.rchecker) 
   | _ => fail "Unsupported domain"
   end in tac.