From 8c697ac826f8bcac956fe8a6c6356a6c459d3c92 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 23 Aug 2011 08:24:10 +0000 Subject: MAJ licence git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1725 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- LICENSE | 33 ++++++++++++++++++--------------- cfrontend/C2C.ml | 3 +++ 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. *) (* *) (* *********************************************************************) -- cgit v1.2.3