From fb50696d492027744c3c9044fd863f93e0a1605c Mon Sep 17 00:00:00 2001
From: Frédéric Besson <frederic.besson@inria.fr>
Date: Fri, 1 Aug 2014 18:42:26 +0200
Subject: micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl
 true)

* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
---
 plugins/micromega/Lia.v   | 10 +++++-----
 plugins/micromega/Psatz.v | 25 +++++++++++++------------
 2 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index add394539..aaa42d1f9 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -24,19 +24,19 @@ Ltac preprocess :=
 
 Ltac lia :=
   preprocess;
-  (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ;
+  xlia ;
   abstract (
       intros __wit __varmap __ff ;
       change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
+      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
 
 Ltac nia :=
   preprocess;
   xnlia ;
   abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
+      intros __wit __varmap __ff ;
+      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
+      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 94b1fe950..b7e277721 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -28,11 +28,11 @@ Ltac preprocess :=
 
 Ltac lia :=
   preprocess;
-  (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ;
+  xlia ;
   abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
+      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
 
 Ltac nia :=
   preprocess;
@@ -40,30 +40,31 @@ Ltac nia :=
   abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
+      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
 
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z =>
     (sos_Z || psatz_Z d) ;
+      abstract(
     intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-    apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+    apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))
   | 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 (intros __wit __varmap __ff ;
+    try (abstract(intros __wit __varmap __ff ;
         change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
+        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
   | 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 (intros __wit __varmap __ff ;
+    try  (abstract(intros __wit __varmap __ff ;
         change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
+        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -77,17 +78,17 @@ Ltac psatzl dom :=
     psatzl_Q ;
     (* 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 ;
+    try (abstract(intros __wit __varmap __ff ;
         change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
+        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
   | R =>
     unfold Rdiv in * ; 
     psatzl_R ;
     (* 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 ;
+    try abstract((intros __wit __varmap __ff ;
         change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
+        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
   | _ => fail "Unsupported domain"
   end in tac.
 
-- 
cgit v1.2.3