diff --git a/theories/base.v b/theories/base.v
index f0964e3cbf3230bc4a3b0676cad4cad3fafbab90..56dcd6acf81dc711512bce067aa436c81bdcb015 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -5,7 +5,6 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, collections, and various other data
 structures. *)
 Global Generalizable All Variables.
-Global Set Asymmetric Patterns.
 Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 Set Default Proof Using "Type".
diff --git a/theories/fin.v b/theories/fin.v
index 4b8cdd0af0de086b221f26f116e68f99bf9f6846..6dc71b127a3effe1b7fe9fd993492376bc2061c9 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -28,7 +28,7 @@ Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
 Notation "10" := (FS 9) : fin_scope.
 
 Fixpoint fin_to_nat {n} (i : fin n) : nat :=
-  match i with 0%fin => 0 | FS _ i => S (fin_to_nat i) end.
+  match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
 Coercion fin_to_nat : fin >-> nat.
 
 Notation fin_of_nat := Fin.of_nat_lt.
@@ -57,7 +57,7 @@ Definition fin_S_inv {n} (P : fin (S n) → Type)
   (H0 : P 0%fin) (HS : ∀ i, P (FS i)) (i : fin (S n)) : P i.
 Proof.
   revert P H0 HS.
-  refine match i with 0%fin => λ _ H0 _, H0 | FS _ i => λ _ _ HS, HS i end.
+  refine match i with 0%fin => λ _ H0 _, H0 | FS i => λ _ _ HS, HS i end.
 Defined.
 
 Ltac inv_fin i :=
diff --git a/theories/finite.v b/theories/finite.v
index aba0ae9267dcf7b63379cf6d7fcd9c1d1aa8e3e1..ab14c0e092bd3098f9486593d00a2fe459fe80b2 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
   Fin.of_nat_lt (encode_lt_card x).
 Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
   match Some_dec (decode_nat i) return _ with
-  | inleft (exist x _) => x | inright _ => _
+  | inleft (exist _ x _) => x | inright _ => _
   end.
 Next Obligation.
   intros A ?? i ?; exfalso.
diff --git a/theories/hlist.v b/theories/hlist.v
index 90a9830fe3cbb4e6e10fa73a680a41991a0efc65..ae4f934180b429c4ebf93f06a92a3da2ed36ad5f 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -14,12 +14,12 @@ Inductive hlist : tlist → Type :=
 Fixpoint tapp (As Bs : tlist) : tlist :=
   match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
 Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
-  match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.
+  match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
 
 Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
-  match xs with hnil => () | hcons _ _ x _ => x end.
+  match xs with hnil => () | hcons x _ => x end.
 Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
-  match xs with hnil => () | hcons _ _ _ xs => xs end.
+  match xs with hnil => () | hcons _ xs => xs end.
 
 Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
   match As with
@@ -43,7 +43,7 @@ Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
   (fix go As xs :=
     match xs in hlist As return himpl As B → B with
     | hnil => λ f, f
-    | hcons A As x xs => λ f, go As xs (f x)
+    | @hcons A As x xs => λ f, go As xs (f x)
     end) _ xs f.
 Coercion hcurry : himpl >-> Funclass.
 
diff --git a/theories/option.v b/theories/option.v
index 9f5b7efb4b9bad18636185ae0adc230ec56f82a4..d50cc7ea0ef185e6e46868c3432186733375665f 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -65,7 +65,7 @@ Proof.
   set (f mx := match mx return P mx → is_Some mx with
     Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
   set (g mx (H : is_Some mx) :=
-    match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
+    match H return P mx with ex_intro _ _ p => eq_rect _ _ I _ (eq_sym p) end).
   assert (∀ mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
   intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
 Qed.
diff --git a/theories/vector.v b/theories/vector.v
index 69b31fe050890ec000072125389cc21568e8dc4c..e46774e74e5570251a5b0d4ff9e0a88daa88732b 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -238,7 +238,7 @@ Qed.
 Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n → vec A n :=
   match i with
   | 0%fin => vec_S_inv _ (λ _ v, x ::: v)
-  | FS _ i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
+  | FS i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
   end.
 
 Lemma vec_to_list_insert {A n} i x (v : vec A n) :