From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 plugins/romega/ReflOmegaCore.v | 39 +++++++++++++++++++++------------------
 1 file changed, 21 insertions(+), 18 deletions(-)

(limited to 'plugins/romega/ReflOmegaCore.v')

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b84cf254..187601fc 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1074,16 +1074,19 @@ Qed.
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_beq t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_bgt t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
@@ -1448,27 +1451,27 @@ Ltac loop t :=
   | (Tint ?X1) => loop X1
   (* Eliminations *)
   | match ?X1 with
-    | EqTerm x x0 => _
-    | LeqTerm x x0 => _
+    | EqTerm _ _ => _
+    | LeqTerm _ _ => _
     | TrueTerm => _
     | FalseTerm => _
-    | Tnot x => _
-    | GeqTerm x x0 => _
-    | GtTerm x x0 => _
-    | LtTerm x x0 => _
-    | NeqTerm x x0 => _
-    | Tor x x0 => _
-    | Tand x x0 => _
-    | Timp x x0 => _
-    | Tprop x => _
+    | Tnot _ => _
+    | GeqTerm _ _ => _
+    | GtTerm _ _ => _
+    | LtTerm _ _ => _
+    | NeqTerm _ _ => _
+    | Tor _ _ => _
+    | Tand _ _ => _
+    | Timp _ _ => _
+    | Tprop _ => _
     end => destruct X1; auto; Simplify
   | match ?X1 with
-    | Tint x => _
-    | (x + x0)%term => _
-    | (x * x0)%term => _
-    | (x - x0)%term => _
-    | (- x)%term => _
-    | [x]%term => _
+    | Tint _ => _
+    | (_ + _)%term => _
+    | (_ * _)%term => _
+    | (_ - _)%term => _
+    | (- _)%term => _
+    | [_]%term => _
     end => destruct X1; auto; Simplify
   | (if beq ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
@@ -1492,7 +1495,7 @@ with Simplify := match goal with
   end.
 
 Ltac prove_stable x th :=
-  match constr:x with
+  match constr:(x) with
   | ?X1 =>
       unfold term_stable, X1; intros; Simplify; simpl;
        apply th
-- 
cgit v1.2.3