From 03bd49e69578665ae33e03300a1277b1c83e1939 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 9 Aug 2016 17:00:04 +0200
Subject: Reduce warning noise when compiling the standard library.

---
 plugins/romega/ReflOmegaCore.v | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

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

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 5e43dfc42..187601fc6 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1451,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
-- 
cgit v1.2.3