diff options
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 37 |
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: *) |