Skip to content

Commit 04f499c

Browse files
xavierleroyxavierleroy
committed
Use the LGPL instead of the GPL for dual-licensed files
The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
1 parent 1f35599 commit 04f499c

File tree

149 files changed

+1171
-860
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

149 files changed

+1171
-860
lines changed

‎LICENSE

+431-268
Large diffs are not rendered by default.

‎Makefile

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
# #
77
# Copyright Institut National de Recherche en Informatique et en #
88
# Automatique. All rights reserved. This file is distributed #
9-
# under the terms of the GNU General Public License as published by #
10-
# the Free Software Foundation, either version 2 of the License, or #
11-
# (at your option) any later version. This file is also distributed #
12-
# under the terms of the INRIA Non-Commercial License Agreement. #
9+
# under the terms of the GNU Lesser General Public License as #
10+
# published by the Free Software Foundation, either version 2.1 of #
11+
# the License, or (at your option) any later version. #
12+
# This file is also distributed under the terms of the #
13+
# INRIA Non-Commercial License Agreement. #
1314
# #
1415
#######################################################################
1516

‎Makefile.extr

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
# #
77
# Copyright Institut National de Recherche en Informatique et en #
88
# Automatique. All rights reserved. This file is distributed #
9-
# under the terms of the GNU General Public License as published by #
10-
# the Free Software Foundation, either version 2 of the License, or #
11-
# (at your option) any later version. This file is also distributed #
12-
# under the terms of the INRIA Non-Commercial License Agreement. #
9+
# under the terms of the GNU Lesser General Public License as #
10+
# published by the Free Software Foundation, either version 2.1 of #
11+
# the License, or (at your option) any later version. #
12+
# This file is also distributed under the terms of the #
13+
# INRIA Non-Commercial License Agreement. #
1314
# #
1415
#######################################################################
1516

‎Makefile.menhir

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
# #
77
# Copyright Institut National de Recherche en Informatique et en #
88
# Automatique. All rights reserved. This file is distributed #
9-
# under the terms of the GNU General Public License as published by #
10-
# the Free Software Foundation, either version 2 of the License, or #
11-
# (at your option) any later version. This file is also distributed #
12-
# under the terms of the INRIA Non-Commercial License Agreement. #
9+
# under the terms of the GNU Lesser General Public License as #
10+
# published by the Free Software Foundation, either version 2.1 of #
11+
# the License, or (at your option) any later version. #
12+
# This file is also distributed under the terms of the #
13+
# INRIA Non-Commercial License Agreement. #
1314
# #
1415
#######################################################################
1516

‎aarch64/Archi.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎aarch64/Builtins1.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎aarch64/CBuiltins.ml

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎aarch64/extractionMachdep.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎arm/Archi.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,11 @@
77
(* *)
88
(* Copyright Institut National de Recherche en Informatique et en *)
99
(* Automatique. All rights reserved. This file is distributed *)
10-
(* under the terms of the GNU General Public License as published by *)
11-
(* the Free Software Foundation, either version 2 of the License, or *)
12-
(* (at your option) any later version. This file is also distributed *)
13-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
10+
(* under the terms of the GNU Lesser General Public License as *)
11+
(* published by the Free Software Foundation, either version 2.1 of *)
12+
(* the License, or (at your option) any later version. *)
13+
(* This file is also distributed under the terms of the *)
14+
(* INRIA Non-Commercial License Agreement. *)
1415
(* *)
1516
(* *********************************************************************)
1617

‎arm/Builtins1.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎arm/CBuiltins.ml

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎arm/extractionMachdep.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎backend/Cminor.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎backend/PrintCminor.ml

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎cfrontend/C2C.ml

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎cfrontend/CPragmas.ml

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎cfrontend/Clight.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎cfrontend/ClightBigstep.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎cfrontend/Cop.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

‎cfrontend/Csem.v

+5-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,11 @@
66
(* *)
77
(* Copyright Institut National de Recherche en Informatique et en *)
88
(* Automatique. All rights reserved. This file is distributed *)
9-
(* under the terms of the GNU General Public License as published by *)
10-
(* the Free Software Foundation, either version 2 of the License, or *)
11-
(* (at your option) any later version. This file is also distributed *)
12-
(* under the terms of the INRIA Non-Commercial License Agreement. *)
9+
(* under the terms of the GNU Lesser General Public License as *)
10+
(* published by the Free Software Foundation, either version 2.1 of *)
11+
(* the License, or (at your option) any later version. *)
12+
(* This file is also distributed under the terms of the *)
13+
(* INRIA Non-Commercial License Agreement. *)
1314
(* *)
1415
(* *********************************************************************)
1516

0 commit comments

Comments
 (0)