Avoid Global Set Asymmetric Patterns (#408)

Instead, add `Set Asymmetric Patterns` to the files that need it,
or use `Arguments` to make inductive types work better with symmetric patterns.

Closes: #403

Author: xavierleroy

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

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 *)

common/Behaviors.v

@@ -25,6 +25,7 @@ Require Import Integers.
 Require Import Smallstep.
 
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (** * Behaviors for program executions *)
 

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]. *)

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.

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 *)

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]:

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.