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