Merge branch 'v8.6'

2 files changed, 18 insertions, 18 deletions

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 864d90a0f..60fe8e762 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -310,7 +310,7 @@ let base_r = function
 let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
   let needed = ref Refset'.empty
   and needed_mps = ref MPset.empty in
-  ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty),
+  ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty),
    (fun r -> needed := Refset'.add (base_r r) !needed),
    (fun mp -> needed_mps := MPset.add mp !needed_mps),
    (fun r -> needed := Refset'.remove (base_r r) !needed),
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