aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--LICENSE2
-rw-r--r--lib/Floataux.ml3
2 files changed, 4 insertions, 1 deletions
diff --git a/LICENSE b/LICENSE
index f9bae5b5..782f2962 100644
--- a/LICENSE
+++ b/LICENSE
@@ -26,7 +26,7 @@ option) any later version:
cfrontend/Csem.v lib/Maps.v
cfrontend/Csyntax.v lib/Parmov.v
common/AST.v lib/Camlcoq.ml
- common/Errors.v
+ common/Errors.v lib/Floataux.ml
common/Events.v
all files in the runtime/ directory
all files in the cparser/ directory
diff --git a/lib/Floataux.ml b/lib/Floataux.ml
index ebea8841..f0db1fa0 100644
--- a/lib/Floataux.ml
+++ b/lib/Floataux.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. *)
(* *)
(* *********************************************************************)