Application des patches envoyés par F. Besson pour micromega

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 16 deletions

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a2b10ebaa..444a590a1 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -33,14 +33,18 @@ Ltac xpsatz dom d :=
     apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | R =>
     (sos_R || psatz_R d) ;
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-    apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+    (* 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 (intros __wit __varmap __ff ;
+        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+        apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
   | Q =>
-      (sos_Q || psatz_Q d) ;
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-    apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+    (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 (intros __wit __varmap __ff ;
+        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+        apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -56,26 +60,27 @@ Ltac psatzl dom :=
     apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | Q =>
     psatzl_Q ;
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-    apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+    (* 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 (intros __wit __varmap __ff ;
+        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+        apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
   | R =>
     psatzl_R ;
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-    apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+    (* 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 (intros __wit __varmap __ff ;
+        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+        apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
   | _ => fail "Unsupported domain"
   end in tac.
 
-
-
 Ltac lia :=
   xlia ;
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
       apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
 
-
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)