6 files changed, 10 insertions, 10 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 82055c4752..f78c0ecc1e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -550,14 +550,14 @@ Ltac intuition_in := repeat (intuition; inv In; inv MapsTo).
    Let's do its job by hand: *)
 
 Ltac join_tac :=
- intros l; induction l as [| ll _ lx ld lr Hlr lh];
-   [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
-     [ | destruct (gt_le_dec lh (rh+2)) as [GT|LE];
+ intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh];
+   [ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join;
+     [ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE];
        [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
            replace (bal u v w z)
            with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
          end
-       | destruct (gt_le_dec rh (lh+2)) as [GT'|LE'];
+       | destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE'];
          [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
              replace (bal u v w z)
              with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto]
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 387ab75362..4179765dca 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1753,7 +1753,7 @@ Qed.
 
 Ltac destr_pggcdn IHn :=
  match goal with |- context [ ggcdn _ ?x ?y ] =>
-  generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl
+  generalize (IHn x y); destruct ggcdn as (?g,(?u,?v)); simpl
  end.
 
 Lemma ggcdn_correct_divisors : forall n a b,
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v
index f3b70f61d2..3d955fec4f 100644
--- a/theories/micromega/Lia.v
+++ b/theories/micromega/Lia.v
@@ -21,7 +21,7 @@ Declare ML Module "micromega_plugin".
 
 
 Ltac zchecker :=
-  intros __wit __varmap __ff ;
+  intros ?__wit ?__varmap ?__ff ;
   exact (ZTautoChecker_sound __ff __wit
                                 (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true)
                                 (@find Z Z0 __varmap)).
diff --git a/theories/micromega/Lqa.v b/theories/micromega/Lqa.v
index 786c9275f0..8a4d59b1bd 100644
--- a/theories/micromega/Lqa.v
+++ b/theories/micromega/Lqa.v
@@ -23,7 +23,7 @@ Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac rchange := 
-  intros __wit __varmap __ff ;
+  intros ?__wit ?__varmap ?__ff ;
   change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
   apply (QTautoChecker_sound __ff __wit).
 
diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v
index 3ac4772ba4..22cef50e0d 100644
--- a/theories/micromega/Lra.v
+++ b/theories/micromega/Lra.v
@@ -23,7 +23,7 @@ Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac rchange := 
-  intros __wit __varmap __ff ;
+  intros ?__wit ?__varmap ?__ff ;
   change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ;
   apply (RTautoChecker_sound __ff __wit).
 
diff --git a/theories/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v
index 89a5ca6740..15b2618e47 100644
--- a/theories/setoid_ring/Field_tac.v
+++ b/theories/setoid_ring/Field_tac.v
@@ -215,7 +215,7 @@ Ltac fold_field_cond req :=
 Ltac simpl_PCond FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); 
+  try (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req;
   try exact I.
@@ -223,7 +223,7 @@ Ltac simpl_PCond FLD :=
 Ltac simpl_PCond_BEURK FLD :=
   let req := get_FldEq FLD in
   let lemma := get_CondLemma FLD in
-  (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
+  (apply lemma; intros ?lock ?lock_def; vm_compute; rewrite lock_def; clear lock_def lock);
   protect_fv "field_cond";
   fold_field_cond req.