11 files changed, 13 insertions, 13 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 08dc5262a..80884c527 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -257,7 +257,7 @@ Qed.
 
 Lemma mapi_inv : forall m x b (f : key -> elt -> elt'),
  MapsTo x b (mapi f m) ->
- exists a, exists y, E.eq y x /\ b = f y a /\ MapsTo x a m.
+ exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m.
 Proof.
 intros; case_eq (find x m); intros.
 exists e.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4dd0e501b..4b823d908 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1652,7 +1652,7 @@ Qed.
 
 Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l,
   Forall2 R l (l1' ++ l2') ->
-  exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
+  exists l1 l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
 Proof.
   induction l1'; intros.
     exists [], l; auto.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 5b3157143..a5d6b6730 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -208,7 +208,7 @@ Proof.
 Qed.
 
 Lemma Ntestbit_spec : forall a n,
-  exists l, exists h, 0<=l<2^n /\
+  exists l h, 0<=l<2^n /\
     a = l + ((if Ntestbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros [|a] n.
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index 8e128215d..77a7c7341 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -141,7 +141,7 @@ Proof.
  rewrite <- add_opp_r, <- mul_opp_l. apply gcd_add_mult_diag_r.
 Qed.
 
-Definition Bezout n m p := exists a, exists b, a*n + b*m == p.
+Definition Bezout n m p := exists a b, a*n + b*m == p.
 
 Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
 Proof.
@@ -250,7 +250,7 @@ Proof.
 Qed.
 
 Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
- exists q, exists r, n == q*r /\ (q | m) /\ (r | p).
+ exists q r, n == q*r /\ (q | m) /\ (r | p).
 Proof.
  intros n m p Hn H.
  assert (G := gcd_nonneg n m).
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 8c1e7b4fa..2c46be4c7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -412,7 +412,7 @@ Qed.
 (** Bitwise operations *)
 
 Lemma testbit_spec : forall a n, 0<=n ->
-  exists l, exists h, (0<=l /\ l<2^n) /\
+  exists l h, (0<=l /\ l<2^n) /\
     a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a n. zify. intros H.
diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v
index 072daa273..a7539bc99 100644
--- a/theories/Numbers/NatInt/NZBits.v
+++ b/theories/Numbers/NatInt/NZBits.v
@@ -42,7 +42,7 @@ Module Type NZBitsSpec
  (Import A : NZOrdAxiomsSig')(Import B : Pow' A)(Import C : Bits' A).
 
  Axiom testbit_spec : forall a n, 0<=n ->
-  exists l, exists h, 0<=l<2^n /\
+  exists l h, 0<=l<2^n /\
     a == l + ((if a.[n] then 1 else 0) + 2*h)*2^n.
  Axiom testbit_neg_r : forall a n, n<0 -> a.[n] = false.
 
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 2ab7413e3..9c01ba8cd 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -59,7 +59,7 @@ Module NZDomainProp (Import NZ:NZDomainSig').
 
 (** We prove that any points in NZ have a common descendant by [succ] *)
 
-Definition common_descendant n m := exists k, exists l, (S^k) n == (S^l) m.
+Definition common_descendant n m := exists k l, (S^k) n == (S^l) m.
 
 Instance common_descendant_wd : Proper (eq==>eq==>iff) common_descendant.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
index 77f23a02b..1340e5124 100644
--- a/theories/Numbers/Natural/Abstract/NGcd.v
+++ b/theories/Numbers/Natural/Abstract/NGcd.v
@@ -72,7 +72,7 @@ Qed.
 (** On natural numbers, we should use a particular form
   for the Bezout identity, since we don't have full subtraction. *)
 
-Definition Bezout n m p := exists a, exists b, a*n == p + b*m.
+Definition Bezout n m p := exists a b, a*n == p + b*m.
 
 Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
 Proof.
@@ -188,7 +188,7 @@ Proof.
 Qed.
 
 Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
- exists q, exists r, n == q*r /\ (q | m) /\ (r | p).
+ exists q r, n == q*r /\ (q | m) /\ (r | p).
 Proof.
  intros n m p Hn H.
  assert (G := gcd_nonneg n m).
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 2802e42be..277223f4b 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -404,7 +404,7 @@ Proof.
 Qed.
 
 Lemma testbit_spec : forall a n,
- exists l, exists h, 0<=l<2^n /\
+ exists l h, 0<=l<2^n /\
   a = l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a n. revert a. induction n; intros a; simpl testbit.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 175b1ad2c..8ee48ba55 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -338,7 +338,7 @@ Qed.
 (** Bitwise operations *)
 
 Lemma testbit_spec : forall a n, 0<=n ->
-  exists l, exists h, (0<=l /\ l<2^n) /\
+  exists l h, (0<=l /\ l<2^n) /\
     a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a n _. zify.
diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v
index 71b647063..028149eb8 100644
--- a/theories/ZArith/Zdigits_def.v
+++ b/theories/ZArith/Zdigits_def.v
@@ -109,7 +109,7 @@ Proof.
 Qed.
 
 Lemma Ztestbit_spec : forall a n, 0<=n ->
-  exists l, exists h, 0<=l<2^n /\
+  exists l h, 0<=l<2^n /\
     a = l + ((if Ztestbit a n then 1 else 0) + 2*h)*2^n.
 Proof.
  intros a [ |n|n] Hn; (now destruct Hn) || clear Hn.