aboutsummaryrefslogtreecommitdiffstats
path: root/common/Behaviors.v
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-24 14:51:15 +0200
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-24 14:51:15 +0200
commite49318b3606d7568d8592887e4278efa696afd10 (patch)
tree99a9a1b883e1db3a4f56e1b5046453817827ceef /common/Behaviors.v
parent2789e6179af061381f5b18a268adb562b28bcb8e (diff)
parentc34d25e011402aedad62b3fe9b7b04989df4522e (diff)
downloadcompcert-kvx-e49318b3606d7568d8592887e4278efa696afd10.tar.gz
compcert-kvx-e49318b3606d7568d8592887e4278efa696afd10.zip
Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10
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 *)