From c9fad7cd7bdc4e79fb06a1d39abfa0d5471623e5 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Wed, 15 Sep 2021 14:00:41 +0200
Subject: 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
---
 lib/Coqlib.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'lib/Coqlib.v')

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index c023bdd5..045fb03a 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.
-- 
cgit