diff --git a/backend/Inlining.v b/backend/Inlining.v
index 7eb0f0fab5..d66d258650 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -293,10 +293,13 @@ Inductive inline_decision (ros: reg + ident) : Type :=
   | Cannot_inline
   | Can_inline (id: ident) (f: function) (P: ros = inr reg id) (Q: fenv!id = Some f).
 
+Arguments Cannot_inline {ros}.
+Arguments Can_inline {ros}.
+
 Program Definition can_inline (ros: reg + ident): inline_decision ros :=
   match ros with
-  | inl r => Cannot_inline _
-  | inr id => match fenv!id with Some f => Can_inline _ id f _ _ | None => Cannot_inline _ end
+  | inl r => Cannot_inline
+  | inr id => match fenv!id with Some f => Can_inline id f _ _ | None => Cannot_inline end
   end.
 
 (** Inlining of a call to function [f].  An appropriate context is
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 7b2c7354b1..e33565103b 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -20,6 +20,8 @@ Require Import Axioms Coqlib Maps Errors.
 Require Import AST Linking.
 Require Archi.
 
+Set Asymmetric Patterns.
+
 Local Open Scope error_monad_scope.
 
 (** * Syntax of types *)
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 023b33e2b3..1f7f62263b 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -25,6 +25,7 @@ Require Import Integers.
 Require Import Smallstep.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (** * Behaviors for program executions *)
 
diff --git a/common/Linking.v b/common/Linking.v
index 089f4fd23a..d23b1028e8 100644
--- a/common/Linking.v
+++ b/common/Linking.v
@@ -869,7 +869,7 @@ Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope.
 Fixpoint compose_passes (l l': Language) (passes: Passes l l') : Pass l l' :=
   match passes in Passes l l' return Pass l l' with
   | pass_nil l => pass_identity l
-  | pass_cons l1 l2 l3 pass1 passes => pass_compose pass1 (compose_passes passes)
+  | pass_cons pass1 passes => pass_compose pass1 (compose_passes passes)
   end.
 
 (** Some more lemmas about [nlist_forall2]. *)
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index c023bdd517..045fb03a2e 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -25,8 +25,6 @@ Require Export List.
 Require Export Bool.
 Require Export Lia.
 
-Global Set Asymmetric Patterns.
-
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
diff --git a/lib/Floats.v b/lib/Floats.v
index f56078aa2a..43caebb0dc 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -26,6 +26,7 @@ Import ListNotations.
 
 Close Scope R_scope.
 Open Scope Z_scope.
+Set Asymmetric Patterns.
 
 Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *)
 Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *)
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 82110bff91..66bb397000 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -20,6 +20,8 @@ Require Import Axioms.
 Require Import Coqlib.
 Require Import Wfsimpl.
 
+Set Asymmetric Patterns.
+
 (** This modules defines several Coq encodings of a general "while" loop.
   The loop is presented in functional style as the iteration
   of a [step] function of type [A -> B + A]:
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 67e4271dfe..1bc2f657f9 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -21,6 +21,7 @@ Require Import Coqlib.
 
 Open Scope nat_scope.
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.