aboutsummaryrefslogtreecommitdiffstats
path: root/lib/UnionFind.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/UnionFind.v')
-rw-r--r--lib/UnionFind.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index ee24a9a7..1c37a35b 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.