summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-23 08:24:10 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-23 08:24:10 +0000
commit8c697ac826f8bcac956fe8a6c6356a6c459d3c92 (patch)
treee808c3d4b5859180d8c3f3066fbf64393ae39b77
parent97a1231b8f3de4d413fc3347f941812860616575 (diff)
MAJ licence
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1725 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--LICENSE33
-rw-r--r--cfrontend/C2C.ml3
2 files changed, 21 insertions, 15 deletions
diff --git a/LICENSE b/LICENSE
index 782f296..99eafdf 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,8 +1,8 @@
All files in this distribution are part of the Compcert verified compiler.
The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009 Institut National de Recherche en Informatique et en
-Automatique (INRIA).
+2008, 2009, 2010, 2011 Institut National de Recherche en Informatique
+et en Automatique (INRIA).
The Compcert verified compiler is distributed under the terms of the
INRIA Non-Commercial License Agreement given below. This is a
@@ -15,19 +15,22 @@ the INRIA Non-Commercial License Agreement and under the Free Software
Foundation GNU General Public License, either version 2 or (at your
option) any later version:
- backend/Cminor.v common/Globalenvs.v
- backend/CMlexer.mli common/Mem.v
- backend/CMlexer.mll common/Smallstep.v
- backend/CMparser.mly common/Switch.v
- backend/CMtypecheck.ml common/Values.v
- backend/CMtypecheck.mli lib/Coqlib.v
- cfrontend/Cil2Csyntax.ml lib/Floats.v
- cfrontend/PrintCsyntax.ml lib/Integers.v
- cfrontend/Csem.v lib/Maps.v
- cfrontend/Csyntax.v lib/Parmov.v
- common/AST.v lib/Camlcoq.ml
- common/Errors.v lib/Floataux.ml
- common/Events.v
+ backend/Cminor.v common/AST.v
+ backend/CMlexer.mli common/Errors.v
+ backend/CMlexer.mll common/Events.v
+ backend/CMparser.mly common/Globalenvs.v
+ backend/CMtypecheck.ml common/Mem.v
+ backend/CMtypecheck.mli common/Smallstep.v
+ cfrontend/C2C.ml common/Switch.v
+ cfrontend/Csem.v common/Values.v
+ cfrontend/Csyntax.v lib/Coqlib.v
+ cfrontend/Cstrategy.v lib/Floats.v
+ cfrontend/Clight.v lib/Integers.v
+ cfrontend/PrintCsyntax.ml lib/Maps.v
+ cfrontend/PrintClight.ml lib/Parmov.v
+ lib/Camlcoq.ml
+ lib/Floataux.ml
+
all files in the runtime/ directory
all files in the cparser/ directory
(except those listed below which are under a BSD license)
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index c6080c3..a516780 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -6,6 +6,9 @@
(* *)
(* 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. *)
(* *)
(* *********************************************************************)