aboutsummaryrefslogtreecommitdiffstats
path: root/common/Behaviors.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Behaviors.v')
-rw-r--r--common/Behaviors.v10
1 files changed, 6 insertions, 4 deletions
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 92bd708f..1f7f6226 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -6,10 +6,11 @@
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation, either version 2 of the License, or *)
-(* (at your option) any later version. This file is also distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* under the terms of the GNU Lesser General Public License as *)
+(* published by the Free Software Foundation, either version 2.1 of *)
+(* the License, or (at your option) any later version. *)
+(* This file is also distributed under the terms of the *)
+(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
@@ -24,6 +25,7 @@ Require Import Integers.
Require Import Smallstep.
Set Implicit Arguments.
+Set Asymmetric Patterns.
(** * Behaviors for program executions *)