aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Coqlib.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r--lib/Coqlib.v2
1 files changed, 0 insertions, 2 deletions
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.