From 6106e043c8a13bf882d2227b3ee80a108305d8df Mon Sep 17 00:00:00 2001
From: Xia Li-yao <Lysxia@users.noreply.github.com>
Date: Thu, 25 Mar 2021 12:21:14 -0400
Subject: Do not depend on projection parameter names  (#388)

coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters.
There was one place in CompCert where one of these automatically-generated names was used.
This commit avoids using this name.
---
 common/Separation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/common/Separation.v b/common/Separation.v
index bf134a18..dcd07ca8 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -870,7 +870,7 @@ Proof.
   exists j', vres2, m2'; intuition auto.
   split; [|split].
 - exact INJ'.
-- apply m_invar with (m0 := m2).
+- apply (m_invar _ m2).
 + apply globalenv_inject_incr with j m1; auto.
 + eapply Mem.unchanged_on_implies; eauto.
   intros; red; intros; red; intros.
-- 
cgit 


From e6744b2bf013158c5158580107530eee65b53b35 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Apr 2021 11:26:31 +0200
Subject: Ensure compatibility with future versions of MenhirLib

After Menhir version 20210310, the `Fail_pr` constructor of the
`parse_result` type becomes `Fail_pr_full` with two extra arguments.

This PR enables CompCert to handle both versions of the `parse_result`
type in MenhirLib.
---
 cparser/Parse.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index d9f9aa1c..3ed193f9 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -72,12 +72,13 @@ let preprocessed_file transfs name sourcefile =
               (fun () ->
                 Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)) ()
            with
-           | Parser.MenhirLibParser.Inter.Fail_pr ->
-                 (* Theoretically impossible : implies inconsistencies
-                    between grammars. *)
-              Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing"
-           | Parser.MenhirLibParser.Inter.Timeout_pr -> assert false
-           | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast) in
+           | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast
+           | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending
+                     on the version of Menhir.
+                     Fail_pr{,_full} means that there's an inconsistency
+                     between the pre-parser and the parser.
+                     Timeout_pr means that we ran for 2^50 steps. *)
+              Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing") in
       let p1 = Timing.time "Elaboration" Elab.elab_file ast in
       Diagnostics.check_errors ();
       Timing.time2 "Emulations" transform_program t p1 name in
-- 
cgit 


From 45af10b3ac30f8e4f5904824259b04df17e1c6b1 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Apr 2021 13:36:23 +0200
Subject: Refactor cparser/Parse.ml

- Use pipeline notation `|>` for legibility and better GC behavior
  (in bytecode at least).
- Introduce auxiliary functions.
- Remove useless function parameters.
- Fix the timing of the "Emulations" pass
  (because of an extra parameter, what was timed took zero time).
---
 cparser/Parse.ml | 60 +++++++++++++++++++++++++++-----------------------------
 1 file changed, 29 insertions(+), 31 deletions(-)

diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 3ed193f9..542ed0d7 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -17,7 +17,7 @@
 
 module CharSet = Set.Make(struct type t = char let compare = compare end)
 
-let transform_program t p name =
+let transform_program t p =
   let run_pass pass flag p =
     if CharSet.mem flag t then begin
       let p = pass p in
@@ -26,12 +26,12 @@ let transform_program t p name =
     end else
       p
   in
-  let p1 = (run_pass StructPassing.program 's'
-  (run_pass PackedStructs.program 'p'
-  (run_pass Unblock.program 'b'
-  (run_pass Bitfields.program 'f'
-     p)))) in
-  Rename.program p1
+    p
+    |> run_pass Bitfields.program 'f'
+    |> run_pass Unblock.program 'b'
+    |> run_pass PackedStructs.program 'p'
+    |> run_pass StructPassing.program 's'
+    |> Rename.program
 
 let parse_transformations s =
   let t = ref CharSet.empty in
@@ -52,35 +52,33 @@ let read_file sourcefile =
   close_in ic;
   text
 
+let parse_string name text =
+  let log_fuel = Camlcoq.Nat.of_int 50 in
+  match
+    Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)
+  with
+  | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) ->
+      (ast: Cabs.definition list)
+  | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending
+            on the version of Menhir.
+            Fail_pr{,_full} means that there's an inconsistency
+            between the pre-parser and the parser.
+            Timeout_pr means that we ran for 2^50 steps. *)
+      Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing"
+
 let preprocessed_file transfs name sourcefile =
   Diagnostics.reset();
+  let check_errors x =
+    Diagnostics.check_errors(); x in
   (* Reading the whole file at once may seem costly, but seems to be
      the simplest / most robust way of accessing the text underlying
      a range of positions. This is used when printing an error message.
      Plus, I note that reading the whole file into memory leads to a
      speed increase: "make -C test" speeds up by 3 seconds out of 40
      on my machine. *)
-  let text = read_file sourcefile in
-  let p =
-      let t = parse_transformations transfs in
-      let log_fuel = Camlcoq.Nat.of_int 50 in
-      let ast : Cabs.definition list =
-          (match Timing.time "Parsing"
-              (* The call to Lexer.tokens_stream results in the pre
-                 parsing of the entire file. This is non-negligeabe,
-                 so we cannot use Timing.time2 *)
-              (fun () ->
-                Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)) ()
-           with
-           | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast
-           | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending
-                     on the version of Menhir.
-                     Fail_pr{,_full} means that there's an inconsistency
-                     between the pre-parser and the parser.
-                     Timeout_pr means that we ran for 2^50 steps. *)
-              Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing") in
-      let p1 = Timing.time "Elaboration" Elab.elab_file ast in
-      Diagnostics.check_errors ();
-      Timing.time2 "Emulations" transform_program t p1 name in
-  Diagnostics.check_errors();
-  p
+  read_file sourcefile
+  |> Timing.time2 "Parsing" parse_string name
+  |> Timing.time "Elaboration" Elab.elab_file
+  |> check_errors
+  |> Timing.time2 "Emulations" transform_program (parse_transformations transfs)
+  |> check_errors
-- 
cgit 


From 0877e32e0bb836a1b3b34d678f0c68f852c55ff3 Mon Sep 17 00:00:00 2001
From: Amos Robinson <amos.robinson@gmail.com>
Date: Tue, 20 Apr 2021 02:02:30 +1000
Subject: Elab bitfields: check size of type <=32bit rather than checking rank
 (#387)

When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.

This rank check caused issues with standard headers that
declare `uint32_t` to be an `unsigned long` rather than an
`unsigned int`. Here, any bitfields declared as `uint32_t` were
failing to compile even though they are still actually 32 bits.

Co-authored-by: Amos Robinson <amos@gh.st>
---
 cparser/Elab.ml                          |  2 +-
 test/regression/Makefile                 |  2 +-
 test/regression/Results/bitfields_uint_t |  1 +
 test/regression/bitfields_uint_t.c       | 22 ++++++++++++++++++++++
 4 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 test/regression/Results/bitfields_uint_t
 create mode 100644 test/regression/bitfields_uint_t.c

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 25e4a980..05717d97 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1001,7 +1001,7 @@ and elab_field_group env = function
             | TInt(ik, _) -> ik
             | TEnum(_, _) -> enum_ikind
             | _ -> ILongLong (* trigger next error message *) in
-          if integer_rank ik > integer_rank IInt then begin
+          if sizeof_ikind ik > sizeof_ikind IInt then begin
             error loc
               "the type of bit-field '%a' must be an integer type no bigger than 'int'" pp_field id;
             None,env
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 61c154a3..698c1392 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -21,7 +21,7 @@ TESTS=int32 int64 floats floats-basics floats-lit \
 # Can run, but only in compiled mode, and have reference output in Results
 
 TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
-  bitfields5 bitfields6 bitfields7 bitfields8 \
+  bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t \
   builtins-common builtins-$(ARCH) packedstruct1 packedstruct2 alignas \
   varargs1 varargs2 varargs3 sections alias aligned
 
diff --git a/test/regression/Results/bitfields_uint_t b/test/regression/Results/bitfields_uint_t
new file mode 100644
index 00000000..f55071d0
--- /dev/null
+++ b/test/regression/Results/bitfields_uint_t
@@ -0,0 +1 @@
+x = { a = 1, b = 2, c = 3, d = 4 }
diff --git a/test/regression/bitfields_uint_t.c b/test/regression/bitfields_uint_t.c
new file mode 100644
index 00000000..3d7fb4e7
--- /dev/null
+++ b/test/regression/bitfields_uint_t.c
@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <stdint.h>
+
+/* Test that uint32 type synonym works.
+   This previously failed for standard headers where uint32 is defined
+   as a (32-bit) unsigned long. */
+
+struct s {
+  uint32_t a: 1;
+  uint32_t b: 2;
+  uint32_t c: 9;
+  uint32_t d: 20;
+};
+
+struct s x = { 1, 2, 3, 4 };
+
+int main()
+{
+  printf("x = { a = %d, b = %d, c = %d, d = %d }\n", x.a, x.b, x.c, x.d);
+}
+
+
-- 
cgit 


From 7563a5df926a4c6fb1489a7a4c847641c8a35095 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Apr 2021 19:07:32 +0200
Subject: Bump minimal Coq version to 8.9.0

This is required to have List.repeat in the standard library (next commit).
---
 configure | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure b/configure
index a3444de8..681249fa 100755
--- a/configure
+++ b/configure
@@ -503,14 +503,14 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1)
+  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.8.0 and 8.13.1"
+            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.1"
             missingtools=true
         fi;;
   "")
-- 
cgit 


From e4542668e6d348e0300e76bb77105af24aff4233 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 19 Apr 2021 19:08:08 +0200
Subject: Use List.repeat from Coq's standard library instead of list_repeat

---
 backend/NeedDomain.v |  2 +-
 common/Globalenvs.v  | 12 ++++++------
 common/Memdata.v     | 18 +++++++++---------
 lib/Coqlib.v         | 20 --------------------
 4 files changed, 16 insertions(+), 36 deletions(-)

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index fc1ae16d..62b8ff90 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -737,7 +737,7 @@ Lemma store_argument_sound:
 Proof.
   intros.
   assert (UNDEF: list_forall2 memval_lessdef
-                     (list_repeat (size_chunk_nat chunk) Undef)
+                     (List.repeat Undef (size_chunk_nat chunk))
                      (encode_val chunk w)).
   {
      rewrite <- (encode_val_length chunk w).
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 40496044..a83f2caf 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -887,7 +887,7 @@ Qed.
 Definition readbytes_as_zero (m: mem) (b: block) (ofs len: Z) : Prop :=
   forall p n,
   ofs <= p -> p + Z.of_nat n <= ofs + len ->
-  Mem.loadbytes m b p (Z.of_nat n) = Some (list_repeat n (Byte Byte.zero)).
+  Mem.loadbytes m b p (Z.of_nat n) = Some (List.repeat (Byte Byte.zero) n).
 
 Lemma store_zeros_loadbytes:
   forall m b p n m',
@@ -901,8 +901,8 @@ Proof.
   + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia.
     rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ.
     replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia.
-    change (list_repeat (S n0) (Byte Byte.zero))
-      with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)).
+    change (List.repeat (Byte Byte.zero) (S n0))
+      with ((Byte Byte.zero :: nil) ++ List.repeat (Byte Byte.zero) n0).
     apply Mem.loadbytes_concat.
     eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p).
     eapply store_zeros_unchanged; eauto. intros; lia.
@@ -924,11 +924,11 @@ Definition bytes_of_init_data (i: init_data): list memval :=
   | Init_int64 n => inj_bytes (encode_int 8%nat (Int64.unsigned n))
   | Init_float32 n => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
   | Init_float64 n => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
-  | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero)
+  | Init_space n => List.repeat (Byte Byte.zero) (Z.to_nat n)
   | Init_addrof id ofs =>
       match find_symbol ge id with
       | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs)
-      | None   => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef
+      | None   => List.repeat Undef (if Archi.ptr64 then 8%nat else 4%nat)
       end
   end.
 
@@ -1020,7 +1020,7 @@ Lemma store_zeros_read_as_zero:
   read_as_zero m' b p n.
 Proof.
   intros; red; intros.
-  transitivity (Some(decode_val chunk (list_repeat (size_chunk_nat chunk) (Byte Byte.zero)))).
+  transitivity (Some(decode_val chunk (List.repeat (Byte Byte.zero) (size_chunk_nat chunk)))).
   apply Mem.loadbytes_load; auto. rewrite size_chunk_conv.
   eapply store_zeros_loadbytes; eauto. rewrite <- size_chunk_conv; auto.
   f_equal. destruct chunk; unfold decode_val; unfold decode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity.
diff --git a/common/Memdata.v b/common/Memdata.v
index 05a3d4ed..411cbc58 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -371,14 +371,14 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
   | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n))
   | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
   | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
-  | Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v
+  | Vptr b ofs, Mint32 => if Archi.ptr64 then List.repeat Undef 4%nat else inj_value Q32 v
   | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
-  | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef
+  | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else List.repeat Undef 8%nat
   | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
   | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
   | _, Many32 => inj_value Q32 v
   | _, Many64 => inj_value Q64 v
-  | _, _ => list_repeat (size_chunk_nat chunk) Undef
+  | _, _ => List.repeat Undef (size_chunk_nat chunk)
   end.
 
 Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
@@ -674,10 +674,10 @@ Local Transparent inj_value.
     constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto.
     intros (b & P & Q); exists b; auto.
   }
-  assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)).
+  assert (D: shape_encoding chunk v (List.repeat Undef (size_chunk_nat chunk))).
   {
     intros. rewrite EQ; simpl; constructor; auto.
-    intros. eapply in_list_repeat; eauto.
+    intros. eapply repeat_spec; eauto.
   }
   generalize (encode_val_length chunk v). intros LEN.
   unfold encode_val; unfold encode_val in LEN;
@@ -882,21 +882,21 @@ Qed.
 
 Lemma repeat_Undef_inject_any:
   forall f vl,
-  list_forall2 (memval_inject f) (list_repeat (length vl) Undef) vl.
+  list_forall2 (memval_inject f) (List.repeat Undef (length vl)) vl.
 Proof.
   induction vl; simpl; constructor; auto. constructor.
 Qed.
 
 Lemma repeat_Undef_inject_encode_val:
   forall f chunk v,
-  list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v).
+  list_forall2 (memval_inject f) (List.repeat Undef (size_chunk_nat chunk)) (encode_val chunk v).
 Proof.
   intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any.
 Qed.
 
 Lemma repeat_Undef_inject_self:
   forall f n,
-  list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef).
+  list_forall2 (memval_inject f) (List.repeat Undef n) (List.repeat Undef n).
 Proof.
   induction n; simpl; constructor; auto. constructor.
 Qed.
@@ -915,7 +915,7 @@ Theorem encode_val_inject:
   Val.inject f v1 v2 ->
   list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
 Proof.
-Local Opaque list_repeat.
+Local Opaque List.repeat.
   intros. inversion H; subst; simpl; destruct chunk;
   auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val.
 - destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self.
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index bd52d20a..e0789078 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1153,26 +1153,6 @@ Proof.
   destruct l; simpl; auto.
 Qed.
 
-(** A list of [n] elements, all equal to [x]. *)
-
-Fixpoint list_repeat {A: Type} (n: nat) (x: A) {struct n} :=
-  match n with
-  | O => nil
-  | S m => x :: list_repeat m x
-  end.
-
-Lemma length_list_repeat:
-  forall (A: Type) n (x: A), length (list_repeat n x) = n.
-Proof.
-  induction n; simpl; intros. auto. decEq; auto.
-Qed.
-
-Lemma in_list_repeat:
-  forall (A: Type) n (x: A) y, In y (list_repeat n x) -> y = x.
-Proof.
-  induction n; simpl; intros. elim H. destruct H; auto.
-Qed.
-
 (** * Definitions and theorems over boolean types *)
 
 Definition proj_sumbool {P Q: Prop} (a: {P} + {Q}) : bool :=
-- 
cgit 


From bb5dab84859088d70074444cfbf0e51f14e3c782 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 23 Apr 2021 18:29:20 +0200
Subject: Move `$` notation in submodule `ClightNotations` and scope
 `clight_scope`

This avoids a nasty conflict with Ltac2 notations as reported in #392.

The old `$` notation in scope `string_scope` was not used yet, AFAIK.

The new submodule and the new scope are the right places to add future
notations to facilitate working with the output of clightgen.

Fixes: #392
---
 exportclight/Clightdefs.v | 34 +++++++++++++++++++++++-----------
 1 file changed, 23 insertions(+), 11 deletions(-)

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 8af920df..f96513d1 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -18,6 +18,8 @@
 From Coq Require Import Ascii String List ZArith.
 From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
 
+(** ** Short names for types *)
+
 Definition tvoid := Tvoid.
 Definition tschar := Tint I8 Signed noattr.
 Definition tuchar := Tint I8 Unsigned noattr.
@@ -56,6 +58,8 @@ Definition talignas (n: N) (ty: type) :=
 Definition tvolatile_alignas (n: N) (ty: type) :=
   tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
 
+(** ** Constructor for programs and compilation units *)
+
 Definition wf_composites (types: list composite_definition) : Prop :=
   match build_composite_env types with OK _ => True | Error _ => False end.
 
@@ -81,6 +85,8 @@ Definition mkprogram (types: list composite_definition)
      prog_comp_env := ce;
      prog_comp_env_eq := EQ |}.
 
+(** ** Encoding character strings as positive numbers *)
+
 (** The following encoding of character strings as positive numbers
     must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
 
@@ -169,17 +175,6 @@ Fixpoint ident_of_string (s: string) : ident :=
   | String c s => append_char_pos c (ident_of_string s)
   end.
 
-(** A convenient notation [$ "ident"] to force evaluation of
-    [ident_of_string "ident"] *)
-
-Ltac ident_of_string s :=
-  let x := constr:(ident_of_string s) in
-  let y := eval compute in x in
-  exact y.
-
-Notation "$ s" := (ltac:(ident_of_string s))
-                  (at level 1, only parsing) : string_scope.
-
 (** The inverse conversion, from encoded strings to strings *)
 
 Section DECODE_BITS.
@@ -289,3 +284,20 @@ Proof.
   intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
   congruence.
 Qed.
+
+(** ** Notations *)
+
+Module ClightNotations.
+
+(** A convenient notation [$ "ident"] to force evaluation of
+    [ident_of_string "ident"] *)
+
+Ltac ident_of_string s :=
+  let x := constr:(ident_of_string s) in
+  let y := eval compute in x in
+  exact y.
+
+Notation "$ s" := (ltac:(ident_of_string s))
+                  (at level 1, only parsing) : clight_scope.
+
+End ClightNotations.
-- 
cgit 


From 1a52f581eb9cc52e5c1862c7e73253016109e1fc Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 23 Apr 2021 18:40:56 +0200
Subject: Remove `-version-file` option from option summary

The `-version-file` option was removed in commit 600803cae, but remained
in the option summary, as reported in #386.
---
 driver/CommonOptions.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index e8a6941c..a816dd41 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -77,7 +77,6 @@ let general_help =
   -v             Print external commands before invoking them
   -timings       Show the time spent in various compiler passes
   -version       Print the version string and exit
-  -version-file <file> Print version inforation to <file> and exit
   -target <value> Generate code for the given target
   -conf <file>   Read configuration from file
   @<file>        Read command line options from <file>
-- 
cgit 


From d36130f936a07773d925e83d595f27f8779cb3f3 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 23 Apr 2021 18:52:42 +0200
Subject: Update the output of clightgen to pick the `$` notation from its new
 place

Follow-up to bb5dab848
---
 exportclight/ExportClight.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 7604175e..3ef2e4d3 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -455,8 +455,10 @@ let print_composite_definition p (Composite(id, su, m, a)) =
 let prologue = "\
 From Coq Require Import String List ZArith.\n\
 From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\
+Import Clightdefs.ClightNotations.\n\
 Local Open Scope Z_scope.\n\
-Local Open Scope string_scope.\n"
+Local Open Scope string_scope.\n\
+Local Open Scope clight_scope.\n"
 
 (* Naming the compiler-generated temporaries occurring in the program *)
 
-- 
cgit 


From 69e175746c27f340f544c329204d6ad030c3c347 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 23 Mar 2021 20:07:22 +0100
Subject: Tentative first fix for offsets of ld/std.

The offsets immediates used in the ld and std instructions must be a
multiple of the word size. This commit changes the two functions which
are used when generating load/stores in Asmgen, accessind and
transl_memory_access.

For accessind one only needs an additional check that the offset is a
multiple of the word size for the case that the high part of the offset
is zero, since otherwise the immediate is loaded into a register anyway.

The transl_memory_access function needs some slightly more complex
adoption. For all variants that do not construct the address in a
register before hand we must check that the offsets are multiples of the
word size and additionally if a symbol is used that the alignment of the
symbol is also a multiple of the word size. Therefore a new parameter is
introduced that allows checking the alignment.

In order to reduce the code duplication for the proofs these two
functions get an additional parameter in order to indicate wether the
offset needs to be a multiple of the word size or not.
Bug 30983
---
 powerpc/Asm.v               |   2 +
 powerpc/Asmgen.v            | 114 ++++++++++++-------
 powerpc/Asmgenproof.v       |  23 +++-
 powerpc/Asmgenproof1.v      | 271 +++++++++++++++++++++++++++-----------------
 powerpc/extractionMachdep.v |   1 +
 5 files changed, 259 insertions(+), 152 deletions(-)

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 93bc31b8..6b1f2232 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -538,6 +538,8 @@ Axiom small_data_area_addressing:
 
 Parameter symbol_is_rel_data: ident -> ptrofs -> bool.
 
+Parameter symbol_is_aligned: ident -> Z -> bool.
+
 (** Armed with the [low_half] and [high_half] functions,
   we can define the evaluation of a symbolic constant.
   Note that for [const_high], integer constants
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 1dca4ba4..0a75ad58 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -190,36 +190,38 @@ Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) :=
 
 (** Accessing slots in the stack frame.  *)
 
+(* For 64 bit load and store the offset needs to be a multiple of word size *)
 Definition accessind {A: Type}
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned : bool)
        (base: ireg) (ofs: ptrofs) (r: A) (k: code) :=
   let ofs := Ptrofs.to_int ofs in
-  if Int.eq (high_s ofs) Int.zero
+  if Int.eq (high_s ofs) Int.zero && (unaligned || (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero))
   then instr1 r (Cint ofs) base :: k
   else loadimm GPR0 ofs (instr2 r base GPR0 :: k).
 
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
   match ty, preg_of dst with
-  | Tint, IR r => OK(accessind Plwz Plwzx base ofs r k)
-  | Tany32, IR r => OK(accessind Plwz_a Plwzx_a base ofs r k)
-  | Tsingle, FR r => OK(accessind Plfs Plfsx base ofs r k)
-  | Tlong, IR r => OK(accessind Pld Pldx base ofs r k)
-  | Tfloat, FR r => OK(accessind Plfd Plfdx base ofs r k)
-  | Tany64, IR r => OK(accessind Pld_a Pldx_a base ofs r k)
-  | Tany64, FR r => OK(accessind Plfd_a Plfdx_a base ofs r k)
+  | Tint, IR r => OK(accessind Plwz Plwzx true base ofs r k)
+  | Tany32, IR r => OK(accessind Plwz_a Plwzx_a true base ofs r k)
+  | Tsingle, FR r => OK(accessind Plfs Plfsx true base ofs r k)
+  | Tlong, IR r => OK(accessind Pld Pldx false base ofs r k)
+  | Tfloat, FR r => OK(accessind Plfd Plfdx  true base ofs r k)
+  | Tany64, IR r => OK(accessind Pld_a Pldx_a false base ofs r k)
+  | Tany64, FR r => OK(accessind Plfd_a Plfdx_a true base ofs r k)
   | _, _ => Error (msg "Asmgen.loadind")
   end.
 
 Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :=
   match ty, preg_of src with
-  | Tint, IR r => OK(accessind Pstw Pstwx base ofs r k)
-  | Tany32, IR r => OK(accessind Pstw_a Pstwx_a base ofs r k)
-  | Tsingle, FR r => OK(accessind Pstfs Pstfsx base ofs r k)
-  | Tlong, IR r => OK(accessind Pstd Pstdx base ofs r k)
-  | Tfloat, FR r => OK(accessind Pstfd Pstfdx base ofs r k)
-  | Tany64, IR r => OK(accessind Pstd_a Pstdx_a base ofs r k)
-  | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a base ofs r k)
+  | Tint, IR r => OK(accessind Pstw Pstwx true base ofs r k)
+  | Tany32, IR r => OK(accessind Pstw_a Pstwx_a true base ofs r k)
+  | Tsingle, FR r => OK(accessind Pstfs Pstfsx true base ofs r k)
+  | Tlong, IR r => OK(accessind Pstd Pstdx false base ofs r k)
+  | Tfloat, FR r => OK(accessind Pstfd Pstfdx true base ofs r k)
+  | Tany64, IR r => OK(accessind Pstd_a Pstdx_a false base ofs r k)
+  | Tany64, FR r => OK(accessind Pstfd_a Pstfdx_a true base ofs r k)
   | _, _ => Error (msg "Asmgen.storeind")
   end.
 
@@ -724,32 +726,48 @@ Definition transl_op
 Definition int_temp_for (r: mreg) :=
   if mreg_eq r R12 then GPR11 else GPR12.
 
+Definition symbol_ofs_word_aligned symb ofs :=
+  let ofs := Ptrofs.to_int ofs in
+  symbol_is_aligned symb 4 && (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero).
+
 Definition transl_memory_access
      (mk1: constant -> ireg -> instruction)
      (mk2: ireg -> ireg -> instruction)
+     (unaligned : bool)
      (addr: addressing) (args: list mreg)
      (temp: ireg) (k: code) :=
   match addr, args with
   | Aindexed ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (if Int.eq (high_s ofs) Int.zero then
-           mk1 (Cint ofs) r1 :: k
-         else
-           Paddis temp r1 (Cint (high_s ofs)) ::
-           mk1 (Cint (low_s ofs)) temp :: k)
+      OK (if unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
+            if Int.eq (high_s ofs) Int.zero then
+               mk1 (Cint ofs) r1 :: k
+             else
+               Paddis temp r1 (Cint (high_s ofs)) ::
+               mk1 (Cint (low_s ofs)) temp :: k
+          else
+            (loadimm GPR0 ofs (mk2 r1 GPR0 :: k)))
   | Aindexed2, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (mk2 r1 r2 :: k)
   | Aglobal symb ofs, nil =>
-      OK (if symbol_is_small_data symb ofs then
-           mk1 (Csymbol_sda symb ofs) GPR0 :: k
+       OK (if symbol_is_small_data symb ofs then
+             if unaligned || symbol_ofs_word_aligned symb ofs then
+               mk1 (Csymbol_sda symb ofs) GPR0 :: k
+             else
+               Paddi temp GPR0 (Csymbol_sda symb ofs) ::
+               mk1 (Cint Int.zero) temp :: k
          else if symbol_is_rel_data symb ofs then
            Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
            Paddi temp temp (Csymbol_rel_low symb ofs) ::
            mk1 (Cint Int.zero) temp :: k
+         else if  unaligned || symbol_ofs_word_aligned symb ofs then
+           Paddis temp GPR0 (Csymbol_high symb ofs) ::
+           mk1 (Csymbol_low symb ofs) temp :: k
          else
            Paddis temp GPR0 (Csymbol_high symb ofs) ::
-           mk1 (Csymbol_low symb ofs) temp :: k)
+           Paddi temp temp (Csymbol_low symb ofs) ::
+           mk1 (Cint Int.zero) temp :: k)
   | Abased symb ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (if symbol_is_small_data symb ofs then
@@ -760,16 +778,24 @@ Definition transl_memory_access
             Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
             Paddi temp temp (Csymbol_rel_low symb ofs) ::
             mk2 temp GPR0 :: k
-          else
+          else if  unaligned || symbol_ofs_word_aligned symb ofs then
             Paddis temp r1 (Csymbol_high symb ofs) ::
-            mk1 (Csymbol_low symb ofs) temp :: k)
+            mk1 (Csymbol_low symb ofs) temp :: k
+          else
+            Pmr GPR0 r1 ::
+            Paddis temp GPR0 (Csymbol_high symb ofs) ::
+            Paddi temp temp (Csymbol_low symb ofs) ::
+            mk2 temp GPR0 :: k)
   | Ainstack ofs, nil =>
       let ofs := Ptrofs.to_int ofs in
-      OK (if Int.eq (high_s ofs) Int.zero then
-           mk1 (Cint ofs) GPR1 :: k
-         else
-           Paddis temp GPR1 (Cint (high_s ofs)) ::
-           mk1 (Cint (low_s ofs)) temp :: k)
+      OK (if  unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
+            if Int.eq (high_s ofs) Int.zero then
+              mk1 (Cint ofs) GPR1 :: k
+            else
+              Paddis temp GPR1 (Cint (high_s ofs)) ::
+              mk1 (Cint (low_s ofs)) temp :: k
+          else
+             addimm temp GPR1 ofs (mk1 (Cint Int.zero) temp :: k))
   | _, _ =>
       Error(msg "Asmgen.transl_memory_access")
   end.
@@ -779,28 +805,28 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
   match chunk with
   | Mint8signed =>
       do r <- ireg_of dst;
-      transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 (Pextsb r r :: k)
+      transl_memory_access (Plbz r) (Plbzx r) true addr args GPR12 (Pextsb r r :: k)
   | Mint8unsigned =>
       do r <- ireg_of dst;
-      transl_memory_access (Plbz r) (Plbzx r) addr args GPR12 k
+      transl_memory_access (Plbz r) (Plbzx r) true addr args GPR12 k
   | Mint16signed =>
       do r <- ireg_of dst;
-      transl_memory_access (Plha r) (Plhax r) addr args GPR12 k
+      transl_memory_access (Plha r) (Plhax r) true addr args GPR12 k
   | Mint16unsigned =>
       do r <- ireg_of dst;
-      transl_memory_access (Plhz r) (Plhzx r) addr args GPR12 k
+      transl_memory_access (Plhz r) (Plhzx r) true addr args GPR12 k
   | Mint32 =>
       do r <- ireg_of dst;
-      transl_memory_access (Plwz r) (Plwzx r) addr args GPR12 k
+      transl_memory_access (Plwz r) (Plwzx r) true addr args GPR12 k
   | Mint64 =>
       do r <- ireg_of dst;
-      transl_memory_access (Pld r) (Pldx r) addr args GPR12 k
+      transl_memory_access (Pld r) (Pldx r) false addr args GPR12 k
   | Mfloat32 =>
       do r <- freg_of dst;
-      transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k
+      transl_memory_access (Plfs r) (Plfsx r) true addr args GPR12 k
   | Mfloat64 =>
       do r <- freg_of dst;
-      transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k
+      transl_memory_access (Plfd r) (Plfdx r) true addr args GPR12 k
   | _ =>
       Error (msg "Asmgen.transl_load")
   end.
@@ -811,22 +837,22 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
   match chunk with
   | Mint8signed | Mint8unsigned =>
       do r <- ireg_of src;
-      transl_memory_access (Pstb r) (Pstbx r) addr args temp k
+      transl_memory_access (Pstb r) (Pstbx r) true addr args temp k
   | Mint16signed | Mint16unsigned =>
       do r <- ireg_of src;
-      transl_memory_access (Psth r) (Psthx r) addr args temp k
+      transl_memory_access (Psth r) (Psthx r) true addr args temp k
   | Mint32  =>
       do r <- ireg_of src;
-      transl_memory_access (Pstw r) (Pstwx r) addr args temp k
+      transl_memory_access (Pstw r) (Pstwx r) true addr args temp k
   | Mint64  =>
       do r <- ireg_of src;
-      transl_memory_access (Pstd r) (Pstdx r) addr args temp k
+      transl_memory_access (Pstd r) (Pstdx r) false addr args temp k
   | Mfloat32 =>
       do r <- freg_of src;
-      transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k
+      transl_memory_access (Pstfs r) (Pstfsx r) true addr args temp k
   | Mfloat64 =>
       do r <- freg_of src;
-      transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k
+      transl_memory_access (Pstfd r) (Pstfdx r) true addr args temp k
   | _ =>
       Error (msg "Asmgen.transl_store")
   end.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 23071756..2730e3d6 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -205,10 +205,13 @@ Remark loadind_label:
   forall base ofs ty dst k c,
   loadind base ofs ty dst k = OK c -> tail_nolabel k c.
 Proof.
-  unfold loadind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *.
+  unfold loadind, accessind ; intros.
+  set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   destruct ty; try discriminate;
   destruct (preg_of dst); try discriminate;
   destruct (Int.eq (high_s ofs') Int.zero);
+  destruct ofs_mod;
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
@@ -216,10 +219,13 @@ Remark storeind_label:
   forall base ofs ty src k c,
   storeind src base ofs ty k = OK c -> tail_nolabel k c.
 Proof.
-  unfold storeind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *.
+  unfold storeind, accessind;
+  intros. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   destruct ty; try discriminate;
   destruct (preg_of src); try discriminate;
   destruct (Int.eq (high_s ofs') Int.zero);
+  destruct ofs_mod;
   TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 Qed.
 
@@ -298,17 +304,22 @@ Qed.
 
 Remark transl_memory_access_label:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
-         addr args temp k c,
-  transl_memory_access mk1 mk2 addr args temp k = OK c ->
+         unaligned addr args temp k c,
+  transl_memory_access mk1 mk2 unaligned addr args temp k = OK c ->
   (forall c r, nolabel (mk1 c r)) ->
   (forall r1 r2, nolabel (mk2 r1 r2)) ->
   tail_nolabel k c.
 Proof.
   unfold transl_memory_access; intros; destruct addr; TailNoLabel.
-  destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
-  destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+  destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero). destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
+  eapply tail_nolabel_trans. apply loadimm_label. TailNoLabel.
+  destruct (symbol_is_small_data i i0). destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+  destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel.
   destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
+  destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel.
+  destruct (unaligned || Int.eq (Int.mods (Ptrofs.to_int i) (Int.repr 4)) Int.zero).
   destruct (Int.eq (high_s (Ptrofs.to_int i)) Int.zero); TailNoLabel.
+  eapply tail_nolabel_trans. eapply addimm_label. TailNoLabel.
 Qed.
 
 Remark transl_epilogue_label:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 89514d62..7268b407 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -805,6 +805,7 @@ Lemma accessind_load_correct:
   forall (A: Type) (inj: A -> preg)
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned: bool)
        (base: ireg) ofs rx chunk v (rs: regset) m k,
   (forall rs m r1 cst r2,
    exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) ->
@@ -813,14 +814,15 @@ Lemma accessind_load_correct:
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR0 -> inj rx <> PC ->
   exists rs',
-     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m
+     exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m
   /\ rs'#(inj rx) = v
   /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   assert (LD: Mem.loadv chunk m (Val.add (rs base) (Vint ofs')) = Some v)
   by (apply loadv_offset_ptr; auto).
-  destruct (Int.eq (high_s ofs') Int.zero).
+  destruct (Int.eq (high_s ofs') Int.zero && ofs_mod).
 - econstructor; split. apply exec_straight_one.
   rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite LD. eauto. unfold nextinstr. repeat Simplif.
@@ -862,6 +864,7 @@ Lemma accessind_store_correct:
   forall (A: Type) (inj: A -> preg)
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned: bool)
        (base: ireg) ofs rx chunk (rs: regset) m m' k,
   (forall rs m r1 cst r2,
    exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) ->
@@ -870,13 +873,14 @@ Lemma accessind_store_correct:
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs (inj rx)) = Some m' ->
   base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 ->
   exists rs',
-     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m'
+     exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   assert (ST: Mem.storev chunk m (Val.add (rs base) (Vint ofs')) (rs (inj rx)) = Some m')
   by (apply storev_offset_ptr; auto).
-  destruct (Int.eq (high_s ofs') Int.zero).
+  destruct (Int.eq (high_s ofs') Int.zero && ofs_mod).
 - econstructor; split. apply exec_straight_one.
   rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite ST. eauto. unfold nextinstr. repeat Simplif.
@@ -1540,8 +1544,8 @@ Qed.
 (** Translation of memory accesses *)
 
 Lemma transl_memory_access_correct:
-  forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m',
-  transl_memory_access mk1 mk2 addr args temp k = OK c ->
+  forall (P: regset -> Prop) mk1 mk2 unaligned addr args temp k c (rs: regset) a m m',
+  transl_memory_access mk1 mk2 unaligned addr args temp k = OK c ->
   eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
   temp <> GPR0 ->
   (forall cst (r1: ireg) (rs1: regset) k,
@@ -1559,111 +1563,174 @@ Lemma transl_memory_access_correct:
 Proof.
   intros until m'; intros TR ADDR TEMP MK1 MK2.
   unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR.
-  (* Aindexed *)
-  case (Int.eq (high_s i) Int.zero).
-  (* Aindexed short *)
-  apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  (* Aindexed long *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  exploit (MK1 (Cint (low_s i)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
-    unfold rs1; Simpl. rewrite Val.add_assoc.
-Transparent Val.add.
-    simpl. rewrite low_high_s. auto.
-    intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  auto. auto.
-  (* Aindexed2 *)
-  apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  (* Aglobal *)
-  destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
-  (* Aglobal from small data *)
-  apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
-  rewrite add_zero_symbol_address. auto.
-  auto.
-  (* Aglobal from relative data *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
-  set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
-  exploit (MK1 (Cint Int.zero) temp rs2).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
-    unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto.
-    intros; unfold rs2, rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto.
-  apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
-  rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
-  unfold rs1; Simpl. apply low_high_half_zero.
-  eexact EX'. auto.
-  (* Aglobal from absolute data *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
-    unfold rs1. Simpl. rewrite low_high_half_zero. auto.
-    intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto.
-  eexact EX'. auto.
-  (* Abased *)
+  - (* Aindexed *)
+    destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s i) Int.zero) |].
+    + (* Aindexed 4 aligned short *)
+      apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    (* Aindexed 4 aligned long *)
+    + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+      exploit (MK1 (Cint (low_s i)) temp rs1 k).
+      simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+      unfold rs1; Simpl. rewrite Val.add_assoc.
+      Transparent Val.add.
+      simpl. rewrite low_high_s. auto.
+      intros; unfold rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'. split. apply exec_straight_step with rs1 m.
+      simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+      auto. auto.
+    + (* Aindexed non 4 aligned *)
+      exploit (loadimm_correct GPR0 i (mk2 x GPR0 :: k) rs).
+      intros (rs' & A & B & C).
+      exploit (MK2 x GPR0 rs').
+      rewrite gpr_or_zero_not_zero; eauto with asmgen.
+      rewrite B. rewrite C; eauto with asmgen. auto.
+      intros.  destruct H as [rs'' [A1 B1]]. exists rs''.
+      split. eapply exec_straight_trans. exact A. exact A1. auto.
+  - (* Aindexed2 *)
+    apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+  - (* Aglobal *)
+    destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
+    + (* Aglobal from small data 4 aligned *)
+      case (unaligned || symbol_ofs_word_aligned i i0).
+      apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
+      rewrite add_zero_symbol_address. auto. auto.
+      (* Aglobal from small data not aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add (gpr_or_zero rs GPR0) (const_low ge (Csymbol_sda i i0))))).
+      exploit (MK1 (Cint Int.zero) temp rs1). rewrite gpr_or_zero_not_zero; auto.
+      unfold const_low. unfold rs1. Simpl.
+      rewrite gpr_or_zero_zero. unfold const_low.
+      rewrite small_data_area_addressing by auto.
+      rewrite add_zero_symbol_address. rewrite Val.add_commut.
+      rewrite add_zero_symbol_address. auto.
+      intros. unfold rs1. Simpl.
+      intros. destruct H as [rs2 [A B]].
+      exists rs2. split. eapply exec_straight_step. reflexivity.
+      reflexivity. eexact A. apply B.
+    + (* relative data *)
+        set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+        set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+        exploit (MK1 (Cint Int.zero) temp rs2).
+        simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+        unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto.
+        intros; unfold rs2, rs1; Simpl.
+        intros [rs' [EX' AG']].
+        exists rs'; split. apply exec_straight_step with rs1 m; auto.
+        apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
+        rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
+        unfold rs1; Simpl. apply low_high_half_zero.
+        eexact EX'. auto.
+    + (* Aglobal from absolute data *)
+      destruct (unaligned || symbol_ofs_word_aligned i i0).
+      (* Aglobal 4 aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+      exploit (MK1 (Csymbol_low i i0) temp rs1).
+      simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+      unfold rs1. Simpl. rewrite low_high_half_zero. auto.
+      intros; unfold rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'; split. apply exec_straight_step with rs1 m; auto.
+      eexact EX'. auto.
+      (* Aglobal non aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+      set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+      exploit (MK1 (Cint Int.zero) temp rs2).
+      simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+      unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address.
+      auto. intros; unfold rs2, rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'; split. apply exec_straight_step with rs1 m; auto.
+      apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
+      rewrite gpr_or_zero_not_zero; auto. f_equal. f_equal. f_equal.
+      unfold rs1; Simpl. apply low_high_half_zero. eexact EX'. auto.
+  -(* Abased *)
   destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ].
-  (* Abased from small data *)
-  set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
-  exploit (MK2 x GPR0 rs1 k).
+  + (* Abased from small data *)
+    set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 x GPR0 rs1 k).
     simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
     unfold rs1; Simpl. rewrite Val.add_commut. auto.
     intros. unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
-  unfold const_low. rewrite small_data_area_addressing; auto.
-  apply add_zero_symbol_address.
-  reflexivity.
-  assumption. assumption.
-  (* Abased from relative data *)
-  set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
-  set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
-  set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
-  exploit (MK2 temp GPR0 rs3).
+    intros [rs' [EX' AG']].
+    exists rs'; split. apply exec_straight_step with rs1 m.
+    unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
+    unfold const_low. rewrite small_data_area_addressing; auto.
+    apply add_zero_symbol_address.
+    reflexivity.
+    assumption. assumption.
+  + (* Abased from relative data *)
+    set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+    set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+    set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 temp GPR0 rs3).
     rewrite gpr_or_zero_not_zero by eauto with asmgen.
     f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
     intros. unfold rs3, rs2, rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
-  apply exec_straight_three with rs1 m rs2 m; auto.
-  simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
-  unfold rs2; Simpl. apply low_high_half_zero.
-  eexact EX'. auto.
-  (* Abased absolute *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1 k).
+    intros [rs' [EX' AG']].
+    exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+    apply exec_straight_three with rs1 m rs2 m; auto.
+    simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+    unfold rs2; Simpl. apply low_high_half_zero.
+    eexact EX'. auto.
+  + (* Abased absolute *)
+    destruct (unaligned || symbol_ofs_word_aligned i i0).
+    (* Abased absolute 4 aligned *)
+    set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
+    exploit (MK1 (Csymbol_low i i0) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
     unfold rs1. Simpl.
     rewrite Val.add_assoc. rewrite low_high_half. rewrite Val.add_commut. auto.
     intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  assumption. assumption.
-  (* Ainstack *)
-  set (ofs := Ptrofs.to_int i) in *.
-  assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))).
-  { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. }
-  destruct (Int.eq (high_s ofs) Int.zero); inv TR.
-  apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
-  exploit (MK1 (Cint (low_s ofs)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; auto.
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
-    congruence.
-    intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  assumption. assumption.
+    intros [rs' [EX' AG']].
+    exists rs'. split. apply exec_straight_step with rs1 m.
+    unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    assumption. assumption.
+    (* Abased absolute non aligned *)
+    set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+    set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+    set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 temp GPR0 rs3).
+    rewrite gpr_or_zero_not_zero by eauto with asmgen.
+    f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
+    intros. unfold rs3, rs2, rs1; Simpl.
+    intros [rs' [EX' AG']].
+    exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+    apply exec_straight_three with rs1 m rs2 m; auto.
+    simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+    unfold rs2; Simpl. apply low_high_half_zero.
+    eexact EX'. auto.
+  - (* Ainstack *)
+    set (ofs := Ptrofs.to_int i) in *.
+    assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))).
+    { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. }
+    destruct (unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s ofs) Int.zero)|]; inv TR.
+    + (* Ainstack short *)
+      apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    + (* Ainstack non short *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
+      exploit (MK1 (Cint (low_s ofs)) temp rs1 k).
+      simpl. rewrite gpr_or_zero_not_zero; auto.
+      unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+      rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
+      congruence.
+      intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+      intros [rs' [EX' AG']].
+      exists rs'. split. apply exec_straight_step with rs1 m.
+      unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+      assumption. assumption.
+    + (* Ainstack non aligned *)
+      exploit (addimm_correct temp GPR1 ofs  (mk1 (Cint Int.zero) temp :: k) rs); eauto with asmgen.
+      intros [rs1 [A [B C]]].
+      exploit (MK1 (Cint Int.zero) temp rs1 k).
+      rewrite gpr_or_zero_not_zero; auto. rewrite B. simpl.
+      destruct (rs GPR1); auto.  simpl. rewrite Ptrofs.add_zero.
+      unfold ofs. rewrite Ptrofs.of_int_to_int. auto. auto.
+      intros. rewrite C; auto. intros [rs2 [EX' AG']].
+      exists rs2. split; auto.
+      eapply exec_straight_trans. eexact A. assumption.
 Qed.
 
+
 (** Translation of loads *)
 
 Lemma transl_load_correct:
@@ -1679,8 +1746,8 @@ Proof.
   intros.
   assert (LD: forall v, Val.lessdef a v -> v = a).
   { intros. inv H2; auto. discriminate H1. }
-  assert (BASE: forall mk1 mk2 k' chunk' v',
-  transl_memory_access mk1 mk2 addr args GPR12 k' = OK c ->
+  assert (BASE: forall mk1 mk2 unaligned k' chunk' v',
+  transl_memory_access mk1 mk2 unaligned addr args GPR12 k' = OK c ->
   Mem.loadv chunk' m a = Some v' ->
   (forall cst (r1: ireg) (rs1: regset),
     exec_instr ge fn (mk1 cst r1) rs1 m =
@@ -1758,8 +1825,8 @@ Local Transparent destroyed_by_store.
     subst src; simpl; congruence.
     change (IR GPR12) with (preg_of R12). red; intros; elim n.
     eapply preg_of_injective; eauto.
-  assert (BASE: forall mk1 mk2 chunk',
-  transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c ->
+  assert (BASE: forall mk1 mk2 unaligned chunk',
+  transl_memory_access mk1 mk2 unaligned addr args (int_temp_for src) k = OK c ->
   Mem.storev chunk' m a (rs (preg_of src)) = Some m' ->
   (forall cst (r1: ireg) (rs1: regset),
     exec_instr ge fn (mk1 cst r1) rs1 m =
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index a3e945bf..5193e453 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -21,6 +21,7 @@ Extract Constant Asm.high_half => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data".
 Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data".
+Extract Constant Asm.symbol_is_aligned => "C2C.atom_is_aligned".
 
 (* Suppression of stupidly big equality functions *)
 Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
-- 
cgit 


From ff88fc9f7b7a208555eace2ad0e7e8be753278b5 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 13 Apr 2021 14:12:04 +0200
Subject: More fixes for ld/std issue.

Volatile load and store are expanded later and also use the ld/std
instructions, therefore the same fixes that are applied as well for
them.
Bug 30983
---
 powerpc/Asmexpand.ml | 51 ++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 40 insertions(+), 11 deletions(-)

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index df712b9d..4cb72c10 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -177,34 +177,56 @@ let expand_builtin_memcpy sz al args =
 let expand_volatile_access
        (mk1: ireg -> constant -> unit)
        (mk2: ireg -> ireg -> unit)
+       ?(ofs_unaligned = true)
        addr temp =
   match addr with
   | BA(IR r) ->
       mk1 r (Cint _0)
   | BA_addrstack ofs ->
-      if offset_in_range ofs then
-        mk1 GPR1 (Cint ofs)
+      if ofs_unaligned || Int.eq (Int.mods ofs _4) _0 then
+        if offset_in_range ofs then
+          mk1 GPR1 (Cint ofs)
+        else begin
+          emit (Paddis(temp, GPR1, Cint (Asmgen.high_s ofs)));
+          mk1 temp (Cint (Asmgen.low_s ofs))
+        end
       else begin
-        emit (Paddis(temp, GPR1, Cint (Asmgen.high_s ofs)));
-        mk1 temp (Cint (Asmgen.low_s ofs))
+        emit (Paddis (temp, GPR1, Cint (Asmgen.high_s ofs)));
+        emit (Paddi (temp, temp, Cint (Asmgen.low_s ofs)));
+        mk1 temp (Cint _0)
       end
   | BA_addrglobal(id, ofs) ->
       if symbol_is_small_data id ofs then
-        mk1 GPR0 (Csymbol_sda(id, ofs))
+        if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then
+          mk1 GPR0 (Csymbol_sda(id, ofs))
+        else begin
+          emit (Paddi (temp, GPR0, (Csymbol_sda (id,ofs))));
+          mk1 temp (Cint _0)
+        end
       else if symbol_is_rel_data id ofs then begin
         emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs)));
         emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs)));
         mk1 temp (Cint _0)
-      end else begin
+      end else if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then begin
         emit (Paddis(temp, GPR0, Csymbol_high(id, ofs)));
         mk1 temp (Csymbol_low(id, ofs))
+      end else begin
+        emit (Paddis (temp, GPR0, (Csymbol_high (id, ofs))));
+        emit (Paddi (temp, temp, (Csymbol_low (id, ofs))));
+        mk1 temp (Cint _0)
       end
   | BA_addptr(BA(IR r), BA_int n) ->
-      if offset_in_range n then
-        mk1 r (Cint n)
+      if ofs_unaligned || Int.eq (Int.mods n _4) _0 then
+        if offset_in_range n then
+          mk1 r (Cint n)
+        else begin
+          emit (Paddis(temp, r, Cint (Asmgen.high_s n)));
+          mk1 temp (Cint (Asmgen.low_s n))
+        end
       else begin
-        emit (Paddis(temp, r, Cint (Asmgen.high_s n)));
-        mk1 temp (Cint (Asmgen.low_s n))
+        emit (Paddis (temp, r, Cint (Asmgen.high_s n)));
+        emit (Paddi (temp, temp, Cint (Asmgen.low_s n)));
+        mk1 temp (Cint _0)
       end
   | BA_addptr(BA_addrglobal(id, ofs), BA(IR r)) ->
       if symbol_is_small_data id ofs then begin
@@ -215,9 +237,14 @@ let expand_volatile_access
         emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs)));
         emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs)));
         mk2 temp GPR0
-      end else begin
+      end else if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then begin
         emit (Paddis(temp, r, Csymbol_high(id, ofs)));
         mk1 temp (Csymbol_low(id, ofs))
+      end else begin
+        emit (Pmr (GPR0, r));
+        emit (Paddis(temp, GPR0, Csymbol_high(id, ofs)));
+        emit (Paddi(temp, temp, Csymbol_low(id, ofs)));
+        mk2 temp GPR0
       end
   | BA_addptr(BA(IR r1), BA(IR r2)) ->
       mk2 r1 r2
@@ -283,6 +310,7 @@ let expand_builtin_vload_1 chunk addr res =
       expand_volatile_access
         (fun r c -> emit (Pld(res, c, r)))
         (fun r1 r2 -> emit (Pldx(res, r1, r2)))
+        ~ofs_unaligned:false
         addr GPR11
   | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) ->
       expand_volatile_access
@@ -346,6 +374,7 @@ let expand_builtin_vstore_1 chunk addr src =
       expand_volatile_access
         (fun r c -> emit (Pstd(src, c, r)))
         (fun r1 r2 -> emit (Pstdx(src, r1, r2)))
+        ~ofs_unaligned:false
         addr temp
   | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) ->
       expand_volatile_access
-- 
cgit 


From 48bc183167c4ce01a5c9ea86e49d60530adf7290 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 27 Apr 2021 11:21:33 +0200
Subject: Support Coq 8.13.2

---
 configure | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure b/configure
index 681249fa..5067f306 100755
--- a/configure
+++ b/configure
@@ -503,14 +503,14 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1)
+  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.1"
+            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2"
             missingtools=true
         fi;;
   "")
-- 
cgit 


From 868da35cd23d47e8c027967148518497f921f829 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 27 Apr 2021 11:22:05 +0200
Subject: MacOS: add a #define __DARWIN_OS_INLINE

Seems necessary for the standard headers of a recent version of XCode.
The actual definition in the standard headers is only for GNUC.
---
 configure | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/configure b/configure
index 5067f306..9b00e1be 100755
--- a/configure
+++ b/configure
@@ -363,7 +363,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         casm_options="-arch x86_64 -c"
         clinker_options="-arch x86_64"
         clinker_needs_no_pie=false
-        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E"
+        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
         ;;
@@ -417,7 +417,7 @@ if test "$arch" = "aarch64"; then
         clinker="${toolprefix}cc"
         clinker_needs_no_pie=false
         cprepro="${toolprefix}cc"
-        cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -Wno-\\#warnings -E"
+        cprepro_options="-std=c99 -arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
         ;;
-- 
cgit 


From d54fef19ae19df47dc9e0d64afdb6a110f5ecdb2 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 10 Nov 2020 19:15:16 +0100
Subject: Emit no entry for variables without init in json.

Variables without init do not generated any assembly code so no entry in
the json AST should be generated. They correspond to extern variables
without initializer that are defined in another compilation unit.
Bug 30112
---
 backend/JsonAST.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index d218e567..8ab874b1 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -114,11 +114,17 @@ let pp_program pp pp_inst prog =
   let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
       match def with
       | Gfun (Internal f) ->
+        (* No assembly is generated for non static inline functions *)
         if not (atom_is_iso_inline_definition ident) then
           vars,(ident,f)::funs
         else
           vars,funs
-      | Gvar v -> (ident,v)::vars,funs
+      | Gvar v ->
+        (* No assembly is generated for variables without init *)
+        if v.gvar_init <> [] then
+          (ident,v)::vars,funs
+        else
+          vars, funs
       | _ -> vars,funs) ([],[]) prog.prog_defs in
   pp_jobject_start pp;
   pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars;
-- 
cgit 


From 2c47585b90858a6782b6e9a88efdb43368708429 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 29 Apr 2021 09:34:49 +0200
Subject: Update Changelog

---
 Changelog | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/Changelog b/Changelog
index f86691a6..bda21a96 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,56 @@
+New features:
+- New port: AArch64 (ARM 64 bits, "Apple silicon") under macOS.
+- Support bitfields of types other than `int`, provided they are no larger
+  than 32 bits (#387)
+
+Optimizations:
+- Improved branch tunneling: optimized conditional branches can
+  introduce further opportunities for tunneling, which are now taken
+  into account.
+
+Usability:
+- Pragmas within functions are now ignored (with a warning) instead of
+  being lifted just before the function like in earlier versions.
+- configure script: add `-mandir` option (#382)
+
+Compiler internals:
+- Finer control of variable initialization in sections.  Now we can
+  put variables initialized with symbol addresses that need relocation
+  in specific sections (e.g. `const_data`).
+- Support re-normalization of function parameters at function entry,
+  as required by the AArch64/ELF ABI.
+- PowerPC 64 bits: remove `Pfcfi`, `Pfcfiu`, `Pfctiu` pseudo-instructions,
+  expanding the corresponding int<->FP conversions during the
+  selection pass instead.
+
+Bug fixing:
+- PowerPC 64 bits: incorrect `ld` and `std` instructions were generated
+  and rejected by the assembler.
+- PowerPC: some variadic functions had the wrong position for their
+  first variadic parameter.
+- RISC-V: fix calling convention in the case of floating-point
+  arguments that are passed in integer registers.
+- AArch64: the default function alignment was incorrect, causing a
+  warning from the LLVM assembler.
+- Pick the correct archiver to build `.a` library archives (#380).
+- x86 32 bits: make sure functions returning structs and unions
+  return the correct pointer in register EAX (#377).
+- PowerPC, ARM, AArch64: updated the registers destroyed by asm
+  pseudo-instructions and built-in functions.
+
+The clightgen tool:
+- Move the `$` notation for Clight identifiers to scope `clight_scope`
+  and submodule `ClightNotations`, to avoid clashes with Ltac2's use of `$`
+  (#392).
+
+Coq development:
+- Compatibility with Coq 8.12.2, 8.13.0, 8.13.1, 8.13.2.
+- Compatibility with Menhir 20210419 and up.
+- Oldest Coq version supported is now 8.9.0.
+- Use the `lia` tactic instead of `omega`.
+- Updated the Flocq library to version 3.4.0.
+
+
 Release 3.8, 2020-11-16
 =======================
 
-- 
cgit 


From 38b0babd5a642cea8912524debc63edc67fda08b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 2 May 2021 17:14:38 +0200
Subject: Fix spurious error on initialization of struct with flexible array
 member

The following is correct but was causing a "wrong type for array initializer"
fatal error.

```
struct s { int n; int d[]; };
void f(void) { struct s x = {0}; }
```

Co-authored-by: Michael Schmidt <github@mschmidt.me>
---
 cparser/Unblock.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index d25f70c6..8530ae01 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -31,6 +31,9 @@ let rec local_initializer env path init k =
       let (ty_elt, sz) =
         match unroll env path.etyp with
         | TArray(ty_elt, Some sz, _) -> (ty_elt, sz)
+        (* We accept empty array initializer for flexible array members, which
+           has size zero *)
+        | TArray(ty_elt, None, _) when il = [] -> (ty_elt, 0L)
         | _ -> Diagnostics.fatal_error Diagnostics.no_loc "wrong type for array initializer" in
       let rec array_init pos il =
         if pos >= sz then k else begin
-- 
cgit 


From 320c55590cc30d4ef5b2c1a226f0f940a6bdb445 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 25 Apr 2021 13:57:47 +0200
Subject: Support __builtin_unreachable

Not yet used for optimizations.
---
 aarch64/Asmexpand.ml | 4 ++++
 arm/Asmexpand.ml     | 4 ++++
 cfrontend/C2C.ml     | 3 +++
 common/Builtins0.v   | 5 +++++
 cparser/Cflow.ml     | 6 +++++-
 powerpc/Asmexpand.ml | 3 +++
 riscV/Asmexpand.ml   | 4 ++++
 x86/Asmexpand.ml     | 5 ++++-
 8 files changed, 32 insertions(+), 2 deletions(-)

diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index 6c80e9d3..d24a9ef6 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -355,8 +355,12 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Byte swap *)
   | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
      emit (Prev(W, res, a1))
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 15cbebec..01b18c37 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -407,8 +407,12 @@ let expand_builtin_inline name args res =
   (* Vararg stuff *)
   | "__builtin_va_start", [BA(IR a)], _ ->
      expand_builtin_va_start a
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index fee3d86e..8b205d19 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -268,6 +268,9 @@ let builtins_generic = {
         (TPtr(TVoid [], []),
           [TPtr(TVoid [], []); TInt(IULong, [])],
           false);
+  (* Optimization hints *)
+    "__builtin_unreachable",
+        (TVoid [], [], false);
   (* Helper functions for int64 arithmetic *)
     "__compcert_i64_dtos",
         (TInt(ILongLong, []),
diff --git a/common/Builtins0.v b/common/Builtins0.v
index d84c9112..2251b3d7 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -341,6 +341,7 @@ Inductive standard_builtin : Type :=
   | BI_i16_bswap
   | BI_i32_bswap
   | BI_i64_bswap
+  | BI_unreachable
   | BI_i64_umulh
   | BI_i64_smulh
   | BI_i64_sdiv
@@ -376,6 +377,7 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
  :: ("__builtin_bswap", BI_i32_bswap)
  :: ("__builtin_bswap32", BI_i32_bswap)
  :: ("__builtin_bswap64", BI_i64_bswap)
+ :: ("__builtin_unreachable", BI_unreachable)
  :: ("__compcert_i64_umulh", BI_i64_umulh)
  :: ("__compcert_i64_smulh", BI_i64_smulh)
  :: ("__compcert_i64_sdiv", BI_i64_sdiv)
@@ -414,6 +416,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
       mksignature (Tlong :: nil) Tlong cc_default
   | BI_i16_bswap =>
       mksignature (Tint :: nil) Tint cc_default
+  | BI_unreachable =>
+      mksignature nil Tvoid cc_default
   | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
       mksignature (Tlong :: Tint :: nil) Tlong cc_default
   | BI_i64_dtos | BI_i64_dtou =>
@@ -448,6 +452,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig
   | BI_i64_bswap =>
     mkbuiltin_n1t Tlong Tlong
                   (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
+  | BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _
   | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
   | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
   | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml
index cc257189..8a2a3fe4 100644
--- a/cparser/Cflow.ml
+++ b/cparser/Cflow.ml
@@ -23,8 +23,12 @@ open Cutil
 module StringSet = Set.Make(String)
 
 (* Functions declared noreturn by the standard *)
+(* We also add our own "__builtin_unreachable" function because, currently,
+   it is difficult to attach attributes to a built-in function. *)
+
 let std_noreturn_functions =
-   ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"]
+   ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit";
+    "__builtin_unreachable"]
 
 (* Statements are abstracted as "flow transformers":
    functions from possible inputs to possible outcomes.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 4cb72c10..e663226f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -793,6 +793,9 @@ let expand_builtin_inline name args res =
   (* no operation *)
   | "__builtin_nop", [], _ ->
       emit (Pori (GPR0, GPR0, Cint _0))
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* atomic operations *)
   | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
       (* Register constraints imposed by Machregs.v *)
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index e8c142e9..dc0ec184 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -646,8 +646,12 @@ let expand_builtin_inline name args res =
                         (fun rl ->
                           emit (Pmulw (rl, X a, X b));
                           emit (Pmulhuw (rh, X a, X b)))
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 14cbb373..d757d7c2 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -487,9 +487,12 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
-  (* no operation *)
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


From 3b448f597344109183c2436d477deed0ed820d6f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 27 Apr 2021 09:27:18 +0200
Subject: Support __builtin_expect

Not yet used for optimizations.

Actually, __builtin_expect is removed during C2C conversion, otherwise
the conversion to type "long" produces inefficient code on 64-bit platforms.
---
 cfrontend/C2C.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 8b205d19..1256043e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -271,6 +271,8 @@ let builtins_generic = {
   (* Optimization hints *)
     "__builtin_unreachable",
         (TVoid [], [], false);
+    "__builtin_expect",
+        (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
   (* Helper functions for int64 arithmetic *)
     "__compcert_i64_dtos",
         (TInt(ILongLong, []),
@@ -992,6 +994,9 @@ let rec convertExpr env e =
       ewrap (Ctyping.eselection (convertExpr env arg1)
                                 (convertExpr env arg2) (convertExpr env arg3))
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, [arg1; arg2]) ->
+      convertExpr env arg1
+
   | C.ECall({edesc = C.EVar {name = "printf"}}, args)
     when !Clflags.option_interp ->
       let targs = convertTypArgs env [] args
-- 
cgit 


From 1f35599abe1b82f565a9a1b1ee03f60df362f22d Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 2 May 2021 19:19:12 +0200
Subject: Fix evaluation order in emulation of bitfield assignment

A bitfield assignment `x.b = f()` is expanded into a read-modify-write
on `x.carrier`.  Wrong results can occur if `x.carrier` is read before
the call to `f()`, and `f` itself modifies a bitfield with the same
carrier `x.carrier`.

In this temporary fix, we play on the evaluation order implemented by
the SimplExpr pass of CompCert (left-to-right for side-effecting
subexpression) to make sure the read part of the read-modify-write
sequence occurs after the evaluation of the right-hand side.

More substantial fixes will be considered later.

Fixes: #395
---
 cparser/Bitfields.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 7a00f719..6d4050f1 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -267,7 +267,7 @@ let bitfield_extract env bf carrier =
 unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
 {
   unsigned int mask = ((1U << sz) - 1) << ofs;
-  return (x & ~mask) | ((y << ofs) & mask);
+  return ((y << ofs) & mask) | (x & ~mask);
 }
 
 If the bitfield is of type _Bool, the new value (y above) must be converted
@@ -284,7 +284,7 @@ let bitfield_assign env bf carrier newval =
     eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in
   let newval_masked = ebinint env Oand newval_shifted msk
   and oldval_masked = ebinint env Oand carrier notmsk in
-  ebinint env Oor oldval_masked newval_masked
+  ebinint env Oor newval_masked oldval_masked
 
 (* Initialize a bitfield *)
 
-- 
cgit 


From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 4 May 2021 10:46:17 +0200
Subject: 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.
---
 LICENSE                      | 699 ++++++++++++++++++++++++++-----------------
 Makefile                     |   9 +-
 Makefile.extr                |   9 +-
 Makefile.menhir              |   9 +-
 aarch64/Archi.v              |   9 +-
 aarch64/Builtins1.v          |   9 +-
 aarch64/CBuiltins.ml         |   9 +-
 aarch64/extractionMachdep.v  |   9 +-
 arm/Archi.v                  |   9 +-
 arm/Builtins1.v              |   9 +-
 arm/CBuiltins.ml             |   9 +-
 arm/extractionMachdep.v      |   9 +-
 backend/Cminor.v             |   9 +-
 backend/PrintCminor.ml       |   9 +-
 cfrontend/C2C.ml             |   9 +-
 cfrontend/CPragmas.ml        |   9 +-
 cfrontend/Clight.v           |   9 +-
 cfrontend/ClightBigstep.v    |   9 +-
 cfrontend/Cop.v              |   9 +-
 cfrontend/Csem.v             |   9 +-
 cfrontend/Cstrategy.v        |   9 +-
 cfrontend/Csyntax.v          |   9 +-
 cfrontend/Ctypes.v           |   9 +-
 cfrontend/Ctyping.v          |   9 +-
 cfrontend/PrintClight.ml     |   9 +-
 cfrontend/PrintCsyntax.ml    |   9 +-
 common/AST.v                 |   9 +-
 common/Behaviors.v           |   9 +-
 common/Builtins.v            |   9 +-
 common/Builtins0.v           |   9 +-
 common/Determinism.v         |   9 +-
 common/Errors.v              |   9 +-
 common/Events.v              |   9 +-
 common/Globalenvs.v          |   9 +-
 common/Linking.v             |   9 +-
 common/Memdata.v             |   9 +-
 common/Memory.v              |   9 +-
 common/Memtype.v             |   9 +-
 common/PrintAST.ml           |   9 +-
 common/Sections.ml           |   9 +-
 common/Sections.mli          |   9 +-
 common/Separation.v          |   9 +-
 common/Smallstep.v           |   9 +-
 common/Subtyping.v           |   9 +-
 common/Switch.v              |   9 +-
 common/Switchaux.ml          |   9 +-
 common/Unityping.v           |   9 +-
 common/Values.v              |   9 +-
 configure                    |   9 +-
 cparser/Bitfields.ml         |   9 +-
 cparser/Bitfields.mli        |   9 +-
 cparser/C.mli                |   9 +-
 cparser/Cabs.v               |   9 +-
 cparser/Cabshelper.ml        |   9 +-
 cparser/Ceval.ml             |   9 +-
 cparser/Ceval.mli            |   9 +-
 cparser/Cflow.ml             |   9 +-
 cparser/Cflow.mli            |   9 +-
 cparser/Checks.ml            |   9 +-
 cparser/Checks.mli           |   9 +-
 cparser/Cleanup.ml           |   9 +-
 cparser/Cleanup.mli          |   9 +-
 cparser/Cprint.ml            |   9 +-
 cparser/Cprint.mli           |   9 +-
 cparser/Cutil.ml             |   9 +-
 cparser/Cutil.mli            |   9 +-
 cparser/Diagnostics.ml       |   9 +-
 cparser/Diagnostics.mli      |   9 +-
 cparser/Elab.ml              |   9 +-
 cparser/Elab.mli             |   9 +-
 cparser/Env.ml               |   9 +-
 cparser/Env.mli              |   9 +-
 cparser/ErrorReports.ml      |   9 +-
 cparser/ErrorReports.mli     |   9 +-
 cparser/ExtendedAsm.ml       |   9 +-
 cparser/GCC.ml               |   9 +-
 cparser/GCC.mli              |   9 +-
 cparser/Lexer.mll            |   9 +-
 cparser/Machine.ml           |   9 +-
 cparser/Machine.mli          |   9 +-
 cparser/PackedStructs.ml     |   9 +-
 cparser/Parse.ml             |   9 +-
 cparser/Parse.mli            |   9 +-
 cparser/Parser.vy            |   9 +-
 cparser/Rename.ml            |   9 +-
 cparser/Rename.mli           |   9 +-
 cparser/StructPassing.ml     |   9 +-
 cparser/StructPassing.mli    |   9 +-
 cparser/Transform.ml         |   9 +-
 cparser/Transform.mli        |   9 +-
 cparser/Unblock.ml           |   9 +-
 cparser/Unblock.mli          |   9 +-
 cparser/deLexer.ml           |   9 +-
 cparser/handcrafted.messages |   9 +-
 cparser/pre_parser.mly       |   9 +-
 cparser/pre_parser_aux.ml    |   9 +-
 cparser/pre_parser_aux.mli   |   9 +-
 exportclight/Clightdefs.v    |   9 +-
 exportclight/Clightgen.ml    |   9 +-
 exportclight/Clightnorm.ml   |   9 +-
 exportclight/ExportClight.ml |   9 +-
 extraction/extraction.v      |   9 +-
 lib/Axioms.v                 |   9 +-
 lib/BoolEqual.v              |   9 +-
 lib/Camlcoq.ml               |   9 +-
 lib/Commandline.ml           |   9 +-
 lib/Commandline.mli          |   9 +-
 lib/Coqlib.v                 |   9 +-
 lib/Decidableplus.v          |   9 +-
 lib/FSetAVLplus.v            |   9 +-
 lib/Floats.v                 |   9 +-
 lib/Heaps.v                  |   9 +-
 lib/IEEE754_extra.v          |   9 +-
 lib/Integers.v               |   9 +-
 lib/Intv.v                   |   9 +-
 lib/IntvSets.v               |   9 +-
 lib/Iteration.v              |   9 +-
 lib/Lattice.v                |   9 +-
 lib/Maps.v                   |   9 +-
 lib/Ordered.v                |   9 +-
 lib/Parmov.v                 |   9 +-
 lib/Postorder.v              |   9 +-
 lib/Printlines.ml            |   9 +-
 lib/Printlines.mli           |   9 +-
 lib/Readconfig.mli           |   9 +-
 lib/Readconfig.mll           |   9 +-
 lib/Responsefile.mli         |   9 +-
 lib/Responsefile.mll         |   9 +-
 lib/Tokenize.mli             |   9 +-
 lib/Tokenize.mll             |   9 +-
 lib/UnionFind.v              |   9 +-
 lib/Wfsimpl.v                |   9 +-
 lib/Zbits.v                  |   9 +-
 powerpc/Archi.v              |   9 +-
 powerpc/Builtins1.v          |   9 +-
 powerpc/CBuiltins.ml         |   9 +-
 powerpc/extractionMachdep.v  |   9 +-
 riscV/Archi.v                |   9 +-
 riscV/Builtins1.v            |   9 +-
 riscV/CBuiltins.ml           |   9 +-
 riscV/extractionMachdep.v    |   9 +-
 tools/modorder.ml            |   9 +-
 tools/ndfun.ml               |   9 +-
 tools/xtime.ml               |   9 +-
 x86/Builtins1.v              |   9 +-
 x86/CBuiltins.ml             |   9 +-
 x86/extractionMachdep.v      |   9 +-
 x86_32/Archi.v               |   9 +-
 x86_64/Archi.v               |   9 +-
 149 files changed, 1171 insertions(+), 860 deletions(-)

diff --git a/LICENSE b/LICENSE
index 61b84219..6a4c62c3 100644
--- a/LICENSE
+++ b/LICENSE
@@ -19,8 +19,8 @@ AbsInt Angewandte Informatik GmbH.
 
 The following files in this distribution are dual-licensed both under
 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:
+Foundation GNU Lesser General Public License, either version 2.1 or
+(at your option) any later version:
 
   all files in the lib/ directory
 
@@ -56,17 +56,17 @@ option) any later version:
   Makefile.extr
   Makefile.menhir
 
-A copy of the GNU General Public License version 2 is included below.
-The choice between the two licenses for the files listed above is left
-to the user.  If you opt for the GNU General Public License, these
-files are free software and can be used both in commercial and
-non-commercial contexts, subject to the terms of the GNU General
-Public License.
+A copy of the GNU Lesser General Public License version 2.1 is
+included below.  The choice between the two licenses for the files
+listed above is left to the user.  If you opt for the GNU Lesser
+General Public License, these files are free software and can be used
+both in commercial and non-commercial contexts, subject to the terms
+of the GNU Lesser General Public License.
 
 The files contained in the flocq/ directory and its subdirectories are
 taken from the Flocq project, http://flocq.gforge.inria.fr/. The files
 contained in the MenhirLib directory are taken from the Menhir
-project, http://gallium.inria.fr/~fpottier/menhir/. The files from the
+project, https://gitlab.inria.fr/fpottier/menhir.  The files from the
 Flocq project and the files in the MenhirLib directory are Copyright
 2010-2019 INRIA and distributed under the terms of the GNU Lesser
 General Public Licence, either version 3 of the licence, or (at your
@@ -170,224 +170,400 @@ INRIA Non-Commercial License Agreement for the CompCert verified compiler
 
 ----------------------------------------------------------------------
 
-                      GNU GENERAL PUBLIC LICENSE
-                         Version 2, June 1991
+                  GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 2.1, February 1999
 
- Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
- 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Copyright (C) 1991, 1999 Free Software Foundation, Inc.
+ 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
  Everyone is permitted to copy and distribute verbatim copies
  of this license document, but changing it is not allowed.
 
-			    Preamble
+[This is the first released version of the Lesser GPL.  It also counts
+ as the successor of the GNU Library Public License, version 2, hence
+ the version number 2.1.]
+
+                            Preamble
 
   The licenses for most software are designed to take away your
 freedom to share and change it.  By contrast, the GNU General Public
-License is intended to guarantee your freedom to share and change free
-software--to make sure the software is free for all its users.  This
-General Public License applies to most of the Free Software
-Foundation's software and to any other program whose authors commit to
-using it.  (Some other Free Software Foundation software is covered by
-the GNU Lesser General Public License instead.)  You can apply it to
-your programs, too.
-
-  When we speak of free software, we are referring to freedom, not
-price.  Our General Public Licenses are designed to make sure that you
-have the freedom to distribute copies of free software (and charge for
-this service if you wish), that you receive source code or can get it
-if you want it, that you can change the software or use pieces of it
-in new free programs; and that you know you can do these things.
+Licenses are intended to guarantee your freedom to share and change
+free software--to make sure the software is free for all its users.
+
+  This license, the Lesser General Public License, applies to some
+specially designated software packages--typically libraries--of the
+Free Software Foundation and other authors who decide to use it.  You
+can use it too, but we suggest you first think carefully about whether
+this license or the ordinary General Public License is the better
+strategy to use in any particular case, based on the explanations below.
+
+  When we speak of free software, we are referring to freedom of use,
+not price.  Our General Public Licenses are designed to make sure that
+you have the freedom to distribute copies of free software (and charge
+for this service if you wish); that you receive source code or can get
+it if you want it; that you can change the software and use pieces of
+it in new free programs; and that you are informed that you can do
+these things.
 
   To protect your rights, we need to make restrictions that forbid
-anyone to deny you these rights or to ask you to surrender the rights.
-These restrictions translate to certain responsibilities for you if you
-distribute copies of the software, or if you modify it.
-
-  For example, if you distribute copies of such a program, whether
-gratis or for a fee, you must give the recipients all the rights that
-you have.  You must make sure that they, too, receive or can get the
-source code.  And you must show them these terms so they know their
-rights.
-
-  We protect your rights with two steps: (1) copyright the software, and
-(2) offer you this license which gives you legal permission to copy,
-distribute and/or modify the software.
-
-  Also, for each author's protection and ours, we want to make certain
-that everyone understands that there is no warranty for this free
-software.  If the software is modified by someone else and passed on, we
-want its recipients to know that what they have is not the original, so
-that any problems introduced by others will not reflect on the original
-authors' reputations.
-
-  Finally, any free program is threatened constantly by software
-patents.  We wish to avoid the danger that redistributors of a free
-program will individually obtain patent licenses, in effect making the
-program proprietary.  To prevent this, we have made it clear that any
-patent must be licensed for everyone's free use or not licensed at all.
+distributors to deny you these rights or to ask you to surrender these
+rights.  These restrictions translate to certain responsibilities for
+you if you distribute copies of the library or if you modify it.
+
+  For example, if you distribute copies of the library, whether gratis
+or for a fee, you must give the recipients all the rights that we gave
+you.  You must make sure that they, too, receive or can get the source
+code.  If you link other code with the library, you must provide
+complete object files to the recipients, so that they can relink them
+with the library after making changes to the library and recompiling
+it.  And you must show them these terms so they know their rights.
+
+  We protect your rights with a two-step method: (1) we copyright the
+library, and (2) we offer you this license, which gives you legal
+permission to copy, distribute and/or modify the library.
+
+  To protect each distributor, we want to make it very clear that
+there is no warranty for the free library.  Also, if the library is
+modified by someone else and passed on, the recipients should know
+that what they have is not the original version, so that the original
+author's reputation will not be affected by problems that might be
+introduced by others.
+
+  Finally, software patents pose a constant threat to the existence of
+any free program.  We wish to make sure that a company cannot
+effectively restrict the users of a free program by obtaining a
+restrictive license from a patent holder.  Therefore, we insist that
+any patent license obtained for a version of the library must be
+consistent with the full freedom of use specified in this license.
+
+  Most GNU software, including some libraries, is covered by the
+ordinary GNU General Public License.  This license, the GNU Lesser
+General Public License, applies to certain designated libraries, and
+is quite different from the ordinary General Public License.  We use
+this license for certain libraries in order to permit linking those
+libraries into non-free programs.
+
+  When a program is linked with a library, whether statically or using
+a shared library, the combination of the two is legally speaking a
+combined work, a derivative of the original library.  The ordinary
+General Public License therefore permits such linking only if the
+entire combination fits its criteria of freedom.  The Lesser General
+Public License permits more lax criteria for linking other code with
+the library.
+
+  We call this license the "Lesser" General Public License because it
+does Less to protect the user's freedom than the ordinary General
+Public License.  It also provides other free software developers Less
+of an advantage over competing non-free programs.  These disadvantages
+are the reason we use the ordinary General Public License for many
+libraries.  However, the Lesser license provides advantages in certain
+special circumstances.
+
+  For example, on rare occasions, there may be a special need to
+encourage the widest possible use of a certain library, so that it becomes
+a de-facto standard.  To achieve this, non-free programs must be
+allowed to use the library.  A more frequent case is that a free
+library does the same job as widely used non-free libraries.  In this
+case, there is little to gain by limiting the free library to free
+software only, so we use the Lesser General Public License.
+
+  In other cases, permission to use a particular library in non-free
+programs enables a greater number of people to use a large body of
+free software.  For example, permission to use the GNU C Library in
+non-free programs enables many more people to use the whole GNU
+operating system, as well as its variant, the GNU/Linux operating
+system.
+
+  Although the Lesser General Public License is Less protective of the
+users' freedom, it does ensure that the user of a program that is
+linked with the Library has the freedom and the wherewithal to run
+that program using a modified version of the Library.
 
   The precise terms and conditions for copying, distribution and
-modification follow.
-
-		    GNU GENERAL PUBLIC LICENSE
+modification follow.  Pay close attention to the difference between a
+"work based on the library" and a "work that uses the library".  The
+former contains code derived from the library, whereas the latter must
+be combined with the library in order to run.
+
+                  GNU LESSER GENERAL PUBLIC LICENSE
    TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
 
-  0. This License applies to any program or other work which contains
-a notice placed by the copyright holder saying it may be distributed
-under the terms of this General Public License.  The "Program", below,
-refers to any such program or work, and a "work based on the Program"
-means either the Program or any derivative work under copyright law:
-that is to say, a work containing the Program or a portion of it,
-either verbatim or with modifications and/or translated into another
-language.  (Hereinafter, translation is included without limitation in
-the term "modification".)  Each licensee is addressed as "you".
-
-Activities other than copying, distribution and modification are not
+  0. This License Agreement applies to any software library or other
+program which contains a notice placed by the copyright holder or
+other authorized party saying it may be distributed under the terms of
+this Lesser General Public License (also called "this License").
+Each licensee is addressed as "you".
+
+  A "library" means a collection of software functions and/or data
+prepared so as to be conveniently linked with application programs
+(which use some of those functions and data) to form executables.
+
+  The "Library", below, refers to any such software library or work
+which has been distributed under these terms.  A "work based on the
+Library" means either the Library or any derivative work under
+copyright law: that is to say, a work containing the Library or a
+portion of it, either verbatim or with modifications and/or translated
+straightforwardly into another language.  (Hereinafter, translation is
+included without limitation in the term "modification".)
+
+  "Source code" for a work means the preferred form of the work for
+making modifications to it.  For a library, complete source code means
+all the source code for all modules it contains, plus any associated
+interface definition files, plus the scripts used to control compilation
+and installation of the library.
+
+  Activities other than copying, distribution and modification are not
 covered by this License; they are outside its scope.  The act of
-running the Program is not restricted, and the output from the Program
-is covered only if its contents constitute a work based on the
-Program (independent of having been made by running the Program).
-Whether that is true depends on what the Program does.
-
-  1. You may copy and distribute verbatim copies of the Program's
-source code as you receive it, in any medium, provided that you
-conspicuously and appropriately publish on each copy an appropriate
-copyright notice and disclaimer of warranty; keep intact all the
-notices that refer to this License and to the absence of any warranty;
-and give any other recipients of the Program a copy of this License
-along with the Program.
-
-You may charge a fee for the physical act of transferring a copy, and
-you may at your option offer warranty protection in exchange for a fee.
-
-  2. You may modify your copy or copies of the Program or any portion
-of it, thus forming a work based on the Program, and copy and
+running a program using the Library is not restricted, and output from
+such a program is covered only if its contents constitute a work based
+on the Library (independent of the use of the Library in a tool for
+writing it).  Whether that is true depends on what the Library does
+and what the program that uses the Library does.
+
+  1. You may copy and distribute verbatim copies of the Library's
+complete source code as you receive it, in any medium, provided that
+you conspicuously and appropriately publish on each copy an
+appropriate copyright notice and disclaimer of warranty; keep intact
+all the notices that refer to this License and to the absence of any
+warranty; and distribute a copy of this License along with the
+Library.
+
+  You may charge a fee for the physical act of transferring a copy,
+and you may at your option offer warranty protection in exchange for a
+fee.
+
+  2. You may modify your copy or copies of the Library or any portion
+of it, thus forming a work based on the Library, and copy and
 distribute such modifications or work under the terms of Section 1
 above, provided that you also meet all of these conditions:
 
-    a) You must cause the modified files to carry prominent notices
+    a) The modified work must itself be a software library.
+
+    b) You must cause the files modified to carry prominent notices
     stating that you changed the files and the date of any change.
 
-    b) You must cause any work that you distribute or publish, that in
-    whole or in part contains or is derived from the Program or any
-    part thereof, to be licensed as a whole at no charge to all third
-    parties under the terms of this License.
-
-    c) If the modified program normally reads commands interactively
-    when run, you must cause it, when started running for such
-    interactive use in the most ordinary way, to print or display an
-    announcement including an appropriate copyright notice and a
-    notice that there is no warranty (or else, saying that you provide
-    a warranty) and that users may redistribute the program under
-    these conditions, and telling the user how to view a copy of this
-    License.  (Exception: if the Program itself is interactive but
-    does not normally print such an announcement, your work based on
-    the Program is not required to print an announcement.)
+    c) You must cause the whole of the work to be licensed at no
+    charge to all third parties under the terms of this License.
+
+    d) If a facility in the modified Library refers to a function or a
+    table of data to be supplied by an application program that uses
+    the facility, other than as an argument passed when the facility
+    is invoked, then you must make a good faith effort to ensure that,
+    in the event an application does not supply such function or
+    table, the facility still operates, and performs whatever part of
+    its purpose remains meaningful.
+
+    (For example, a function in a library to compute square roots has
+    a purpose that is entirely well-defined independent of the
+    application.  Therefore, Subsection 2d requires that any
+    application-supplied function or table used by this function must
+    be optional: if the application does not supply it, the square
+    root function must still compute square roots.)
 
 These requirements apply to the modified work as a whole.  If
-identifiable sections of that work are not derived from the Program,
+identifiable sections of that work are not derived from the Library,
 and can be reasonably considered independent and separate works in
 themselves, then this License, and its terms, do not apply to those
 sections when you distribute them as separate works.  But when you
 distribute the same sections as part of a whole which is a work based
-on the Program, the distribution of the whole must be on the terms of
+on the Library, the distribution of the whole must be on the terms of
 this License, whose permissions for other licensees extend to the
-entire whole, and thus to each and every part regardless of who wrote it.
+entire whole, and thus to each and every part regardless of who wrote
+it.
 
 Thus, it is not the intent of this section to claim rights or contest
 your rights to work written entirely by you; rather, the intent is to
 exercise the right to control the distribution of derivative or
-collective works based on the Program.
+collective works based on the Library.
 
-In addition, mere aggregation of another work not based on the Program
-with the Program (or with a work based on the Program) on a volume of
+In addition, mere aggregation of another work not based on the Library
+with the Library (or with a work based on the Library) on a volume of
 a storage or distribution medium does not bring the other work under
 the scope of this License.
 
-  3. You may copy and distribute the Program (or a work based on it,
-under Section 2) in object code or executable form under the terms of
-Sections 1 and 2 above provided that you also do one of the following:
-
-    a) Accompany it with the complete corresponding machine-readable
-    source code, which must be distributed under the terms of Sections
-    1 and 2 above on a medium customarily used for software interchange; or,
-
-    b) Accompany it with a written offer, valid for at least three
-    years, to give any third party, for a charge no more than your
-    cost of physically performing source distribution, a complete
-    machine-readable copy of the corresponding source code, to be
-    distributed under the terms of Sections 1 and 2 above on a medium
-    customarily used for software interchange; or,
-
-    c) Accompany it with the information you received as to the offer
-    to distribute corresponding source code.  (This alternative is
-    allowed only for noncommercial distribution and only if you
-    received the program in object code or executable form with such
-    an offer, in accord with Subsection b above.)
-
-The source code for a work means the preferred form of the work for
-making modifications to it.  For an executable work, complete source
-code means all the source code for all modules it contains, plus any
-associated interface definition files, plus the scripts used to
-control compilation and installation of the executable.  However, as a
-special exception, the source code distributed need not include
-anything that is normally distributed (in either source or binary
-form) with the major components (compiler, kernel, and so on) of the
-operating system on which the executable runs, unless that component
-itself accompanies the executable.
-
-If distribution of executable or object code is made by offering
-access to copy from a designated place, then offering equivalent
-access to copy the source code from the same place counts as
-distribution of the source code, even though third parties are not
+  3. You may opt to apply the terms of the ordinary GNU General Public
+License instead of this License to a given copy of the Library.  To do
+this, you must alter all the notices that refer to this License, so
+that they refer to the ordinary GNU General Public License, version 2,
+instead of to this License.  (If a newer version than version 2 of the
+ordinary GNU General Public License has appeared, then you can specify
+that version instead if you wish.)  Do not make any other change in
+these notices.
+
+  Once this change is made in a given copy, it is irreversible for
+that copy, so the ordinary GNU General Public License applies to all
+subsequent copies and derivative works made from that copy.
+
+  This option is useful when you wish to copy part of the code of
+the Library into a program that is not a library.
+
+  4. You may copy and distribute the Library (or a portion or
+derivative of it, under Section 2) in object code or executable form
+under the terms of Sections 1 and 2 above provided that you accompany
+it with the complete corresponding machine-readable source code, which
+must be distributed under the terms of Sections 1 and 2 above on a
+medium customarily used for software interchange.
+
+  If distribution of object code is made by offering access to copy
+from a designated place, then offering equivalent access to copy the
+source code from the same place satisfies the requirement to
+distribute the source code, even though third parties are not
 compelled to copy the source along with the object code.
 
-  4. You may not copy, modify, sublicense, or distribute the Program
-except as expressly provided under this License.  Any attempt
-otherwise to copy, modify, sublicense or distribute the Program is
-void, and will automatically terminate your rights under this License.
-However, parties who have received copies, or rights, from you under
-this License will not have their licenses terminated so long as such
-parties remain in full compliance.
-
-  5. You are not required to accept this License, since you have not
+  5. A program that contains no derivative of any portion of the
+Library, but is designed to work with the Library by being compiled or
+linked with it, is called a "work that uses the Library".  Such a
+work, in isolation, is not a derivative work of the Library, and
+therefore falls outside the scope of this License.
+
+  However, linking a "work that uses the Library" with the Library
+creates an executable that is a derivative of the Library (because it
+contains portions of the Library), rather than a "work that uses the
+library".  The executable is therefore covered by this License.
+Section 6 states terms for distribution of such executables.
+
+  When a "work that uses the Library" uses material from a header file
+that is part of the Library, the object code for the work may be a
+derivative work of the Library even though the source code is not.
+Whether this is true is especially significant if the work can be
+linked without the Library, or if the work is itself a library.  The
+threshold for this to be true is not precisely defined by law.
+
+  If such an object file uses only numerical parameters, data
+structure layouts and accessors, and small macros and small inline
+functions (ten lines or less in length), then the use of the object
+file is unrestricted, regardless of whether it is legally a derivative
+work.  (Executables containing this object code plus portions of the
+Library will still fall under Section 6.)
+
+  Otherwise, if the work is a derivative of the Library, you may
+distribute the object code for the work under the terms of Section 6.
+Any executables containing that work also fall under Section 6,
+whether or not they are linked directly with the Library itself.
+
+  6. As an exception to the Sections above, you may also combine or
+link a "work that uses the Library" with the Library to produce a
+work containing portions of the Library, and distribute that work
+under terms of your choice, provided that the terms permit
+modification of the work for the customer's own use and reverse
+engineering for debugging such modifications.
+
+  You must give prominent notice with each copy of the work that the
+Library is used in it and that the Library and its use are covered by
+this License.  You must supply a copy of this License.  If the work
+during execution displays copyright notices, you must include the
+copyright notice for the Library among them, as well as a reference
+directing the user to the copy of this License.  Also, you must do one
+of these things:
+
+    a) Accompany the work with the complete corresponding
+    machine-readable source code for the Library including whatever
+    changes were used in the work (which must be distributed under
+    Sections 1 and 2 above); and, if the work is an executable linked
+    with the Library, with the complete machine-readable "work that
+    uses the Library", as object code and/or source code, so that the
+    user can modify the Library and then relink to produce a modified
+    executable containing the modified Library.  (It is understood
+    that the user who changes the contents of definitions files in the
+    Library will not necessarily be able to recompile the application
+    to use the modified definitions.)
+
+    b) Use a suitable shared library mechanism for linking with the
+    Library.  A suitable mechanism is one that (1) uses at run time a
+    copy of the library already present on the user's computer system,
+    rather than copying library functions into the executable, and (2)
+    will operate properly with a modified version of the library, if
+    the user installs one, as long as the modified version is
+    interface-compatible with the version that the work was made with.
+
+    c) Accompany the work with a written offer, valid for at
+    least three years, to give the same user the materials
+    specified in Subsection 6a, above, for a charge no more
+    than the cost of performing this distribution.
+
+    d) If distribution of the work is made by offering access to copy
+    from a designated place, offer equivalent access to copy the above
+    specified materials from the same place.
+
+    e) Verify that the user has already received a copy of these
+    materials or that you have already sent this user a copy.
+
+  For an executable, the required form of the "work that uses the
+Library" must include any data and utility programs needed for
+reproducing the executable from it.  However, as a special exception,
+the materials to be distributed need not include anything that is
+normally distributed (in either source or binary form) with the major
+components (compiler, kernel, and so on) of the operating system on
+which the executable runs, unless that component itself accompanies
+the executable.
+
+  It may happen that this requirement contradicts the license
+restrictions of other proprietary libraries that do not normally
+accompany the operating system.  Such a contradiction means you cannot
+use both them and the Library together in an executable that you
+distribute.
+
+  7. You may place library facilities that are a work based on the
+Library side-by-side in a single library together with other library
+facilities not covered by this License, and distribute such a combined
+library, provided that the separate distribution of the work based on
+the Library and of the other library facilities is otherwise
+permitted, and provided that you do these two things:
+
+    a) Accompany the combined library with a copy of the same work
+    based on the Library, uncombined with any other library
+    facilities.  This must be distributed under the terms of the
+    Sections above.
+
+    b) Give prominent notice with the combined library of the fact
+    that part of it is a work based on the Library, and explaining
+    where to find the accompanying uncombined form of the same work.
+
+  8. You may not copy, modify, sublicense, link with, or distribute
+the Library except as expressly provided under this License.  Any
+attempt otherwise to copy, modify, sublicense, link with, or
+distribute the Library is void, and will automatically terminate your
+rights under this License.  However, parties who have received copies,
+or rights, from you under this License will not have their licenses
+terminated so long as such parties remain in full compliance.
+
+  9. You are not required to accept this License, since you have not
 signed it.  However, nothing else grants you permission to modify or
-distribute the Program or its derivative works.  These actions are
+distribute the Library or its derivative works.  These actions are
 prohibited by law if you do not accept this License.  Therefore, by
-modifying or distributing the Program (or any work based on the
-Program), you indicate your acceptance of this License to do so, and
+modifying or distributing the Library (or any work based on the
+Library), you indicate your acceptance of this License to do so, and
 all its terms and conditions for copying, distributing or modifying
-the Program or works based on it.
+the Library or works based on it.
 
-  6. Each time you redistribute the Program (or any work based on the
-Program), the recipient automatically receives a license from the
-original licensor to copy, distribute or modify the Program subject to
-these terms and conditions.  You may not impose any further
+  10. Each time you redistribute the Library (or any work based on the
+Library), the recipient automatically receives a license from the
+original licensor to copy, distribute, link with or modify the Library
+subject to these terms and conditions.  You may not impose any further
 restrictions on the recipients' exercise of the rights granted herein.
-You are not responsible for enforcing compliance by third parties to
+You are not responsible for enforcing compliance by third parties with
 this License.
-
-  7. If, as a consequence of a court judgment or allegation of patent
+
+  11. If, as a consequence of a court judgment or allegation of patent
 infringement or for any other reason (not limited to patent issues),
 conditions are imposed on you (whether by court order, agreement or
 otherwise) that contradict the conditions of this License, they do not
 excuse you from the conditions of this License.  If you cannot
 distribute so as to satisfy simultaneously your obligations under this
 License and any other pertinent obligations, then as a consequence you
-may not distribute the Program at all.  For example, if a patent
-license would not permit royalty-free redistribution of the Program by
+may not distribute the Library at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Library by
 all those who receive copies directly or indirectly through you, then
 the only way you could satisfy both it and this License would be to
-refrain entirely from distribution of the Program.
+refrain entirely from distribution of the Library.
 
-If any portion of this section is held invalid or unenforceable under
-any particular circumstance, the balance of the section is intended to
-apply and the section as a whole is intended to apply in other
-circumstances.
+If any portion of this section is held invalid or unenforceable under any
+particular circumstance, the balance of the section is intended to apply,
+and the section as a whole is intended to apply in other circumstances.
 
 It is not the purpose of this section to induce you to infringe any
 patents or other property right claims or to contest validity of any
 such claims; this section has the sole purpose of protecting the
-integrity of the free software distribution system, which is
+integrity of the free software distribution system which is
 implemented by public license practices.  Many people have made
 generous contributions to the wide range of software distributed
 through that system in reliance on consistent application of that
@@ -398,117 +574,104 @@ impose that choice.
 This section is intended to make thoroughly clear what is believed to
 be a consequence of the rest of this License.
 
-  8. If the distribution and/or use of the Program is restricted in
+  12. If the distribution and/or use of the Library is restricted in
 certain countries either by patents or by copyrighted interfaces, the
-original copyright holder who places the Program under this License
-may add an explicit geographical distribution limitation excluding
-those countries, so that distribution is permitted only in or among
-countries not thus excluded.  In such case, this License incorporates
-the limitation as if written in the body of this License.
-
-  9. The Free Software Foundation may publish revised and/or new versions
-of the General Public License from time to time.  Such new versions will
-be similar in spirit to the present version, but may differ in detail to
-address new problems or concerns.
-
-Each version is given a distinguishing version number.  If the Program
-specifies a version number of this License which applies to it and "any
-later version", you have the option of following the terms and conditions
-either of that version or of any later version published by the Free
-Software Foundation.  If the Program does not specify a version number of
-this License, you may choose any version ever published by the Free Software
-Foundation.
-
-  10. If you wish to incorporate parts of the Program into other free
-programs whose distribution conditions are different, write to the author
-to ask for permission.  For software which is copyrighted by the Free
-Software Foundation, write to the Free Software Foundation; we sometimes
-make exceptions for this.  Our decision will be guided by the two goals
-of preserving the free status of all derivatives of our free software and
-of promoting the sharing and reuse of software generally.
-
-			    NO WARRANTY
-
-  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
-FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN
-OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
-PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
-OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
-MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS
-TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE
-PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
-REPAIR OR CORRECTION.
-
-  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
-WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
-REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
-INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
-OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
-TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
-YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
-PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
-POSSIBILITY OF SUCH DAMAGES.
-
-		     END OF TERMS AND CONDITIONS
-
-	    How to Apply These Terms to Your New Programs
-
-  If you develop a new program, and you want it to be of the greatest
-possible use to the public, the best way to achieve this is to make it
-free software which everyone can redistribute and change under these terms.
-
-  To do so, attach the following notices to the program.  It is safest
-to attach them to the start of each source file to most effectively
-convey the exclusion of warranty; and each file should have at least
-the "copyright" line and a pointer to where the full notice is found.
-
-    <one line to give the program's name and a brief idea of what it does.>
+original copyright holder who places the Library under this License may add
+an explicit geographical distribution limitation excluding those countries,
+so that distribution is permitted only in or among countries not thus
+excluded.  In such case, this License incorporates the limitation as if
+written in the body of this License.
+
+  13. The Free Software Foundation may publish revised and/or new
+versions of the Lesser General Public License from time to time.
+Such new versions will be similar in spirit to the present version,
+but may differ in detail to address new problems or concerns.
+
+Each version is given a distinguishing version number.  If the Library
+specifies a version number of this License which applies to it and
+"any later version", you have the option of following the terms and
+conditions either of that version or of any later version published by
+the Free Software Foundation.  If the Library does not specify a
+license version number, you may choose any version ever published by
+the Free Software Foundation.
+
+  14. If you wish to incorporate parts of the Library into other free
+programs whose distribution conditions are incompatible with these,
+write to the author to ask for permission.  For software which is
+copyrighted by the Free Software Foundation, write to the Free
+Software Foundation; we sometimes make exceptions for this.  Our
+decision will be guided by the two goals of preserving the free status
+of all derivatives of our free software and of promoting the sharing
+and reuse of software generally.
+
+                            NO WARRANTY
+
+  15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
+WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.
+EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR
+OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY
+KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
+LIBRARY IS WITH YOU.  SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
+THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
+WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
+AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
+FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
+CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
+LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
+RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
+FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
+SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGES.
+
+                     END OF TERMS AND CONDITIONS
+
+           How to Apply These Terms to Your New Libraries
+
+  If you develop a new library, and you want it to be of the greatest
+possible use to the public, we recommend making it free software that
+everyone can redistribute and change.  You can do so by permitting
+redistribution under these terms (or, alternatively, under the terms of the
+ordinary General Public License).
+
+  To apply these terms, attach the following notices to the library.  It is
+safest to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least the
+"copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the library's name and a brief idea of what it does.>
     Copyright (C) <year>  <name of author>
 
-    This program is free software; you can redistribute it and/or modify
-    it 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 library is free software; you can redistribute it and/or
+    modify it 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 program is distributed in the hope that it will be useful,
+    This library is distributed in the hope that it will be useful,
     but WITHOUT ANY WARRANTY; without even the implied warranty of
-    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-    GNU General Public License for more details.
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+    Lesser General Public License for more details.
 
-    You should have received a copy of the GNU General Public License along
-    with this program; if not, write to the Free Software Foundation, Inc.,
-    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+    You should have received a copy of the GNU Lesser General Public
+    License along with this library; if not, write to the Free Software
+    Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
 
 Also add information on how to contact you by electronic and paper mail.
 
-If the program is interactive, make it output a short notice like this
-when it starts in an interactive mode:
-
-    Gnomovision version 69, Copyright (C) year name of author
-    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
-    This is free software, and you are welcome to redistribute it
-    under certain conditions; type `show c' for details.
-
-The hypothetical commands `show w' and `show c' should show the appropriate
-parts of the General Public License.  Of course, the commands you use may
-be called something other than `show w' and `show c'; they could even be
-mouse-clicks or menu items--whatever suits your program.
-
 You should also get your employer (if you work as a programmer) or your
-school, if any, to sign a "copyright disclaimer" for the program, if
+school, if any, to sign a "copyright disclaimer" for the library, if
 necessary.  Here is a sample; alter the names:
 
-  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
-  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the
+  library `Frob' (a library for tweaking knobs) written by James Random Hacker.
 
-  <signature of Ty Coon>, 1 April 1989
+  <signature of Ty Coon>, 1 April 1990
   Ty Coon, President of Vice
 
-This General Public License does not permit incorporating your program into
-proprietary programs.  If your program is a subroutine library, you may
-consider it more useful to permit linking proprietary applications with the
-library.  If this is what you want to do, use the GNU Lesser General
-Public License instead of this License.
+That's all there is to it!
 
 ----------------------------------------------------------------------
 
diff --git a/Makefile b/Makefile
index d0b0029a..a0f9fde6 100644
--- a/Makefile
+++ b/Makefile
@@ -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.                            #
 #                                                                     #
 #######################################################################
 
diff --git a/Makefile.extr b/Makefile.extr
index 23e01614..a8949820 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -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.                            #
 #                                                                     #
 #######################################################################
 
diff --git a/Makefile.menhir b/Makefile.menhir
index 7909b2f6..7687d3ed 100644
--- a/Makefile.menhir
+++ b/Makefile.menhir
@@ -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.                            #
 #                                                                     #
 #######################################################################
 
diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index 91e91673..4911db73 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v
index 53c83d7e..cd6f8cc4 100644
--- a/aarch64/Builtins1.v
+++ b/aarch64/Builtins1.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml
index 4cfb7edf..80d66310 100644
--- a/aarch64/CBuiltins.ml
+++ b/aarch64/CBuiltins.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index 5b81ed4c..ae0006bc 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/arm/Archi.v b/arm/Archi.v
index 2ca79710..c4cb5496 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/arm/Builtins1.v b/arm/Builtins1.v
index 53c83d7e..cd6f8cc4 100644
--- a/arm/Builtins1.v
+++ b/arm/Builtins1.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 6462a8c5..ed21b78f 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v
index a82cf749..5fee431c 100644
--- a/arm/extractionMachdep.v
+++ b/arm/extractionMachdep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/backend/Cminor.v b/backend/Cminor.v
index cf0ba314..1618866e 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index c9a6d399..59b340f7 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 1256043e..6fce9764 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 22ab2b5a..08d0aa6c 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 239ca370..3b21be28 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 92457586..644c4c6c 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 143e87a3..f6524124 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 4fa70ae2..724c1c9e 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 30e5c2ae..6365f85c 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index e3e2c1e9..19bc2ec3 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 0de5075c..bcd8d350 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 87e3506c..5f0a3e5b 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 0e735d2d..a9ecb342 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index c49f6cd4..75c85d60 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/AST.v b/common/AST.v
index 7ccbb6cc..2259d74c 100644
--- a/common/AST.v
+++ b/common/AST.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Behaviors.v b/common/Behaviors.v
index 92bd708f..023b33e2 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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Builtins.v b/common/Builtins.v
index 476b541e..facff726 100644
--- a/common/Builtins.v
+++ b/common/Builtins.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Builtins0.v b/common/Builtins0.v
index 2251b3d7..384dde1e 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Determinism.v b/common/Determinism.v
index 7fa01c2d..c8c90782 100644
--- a/common/Determinism.v
+++ b/common/Determinism.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Errors.v b/common/Errors.v
index 6807735a..bf72f12b 100644
--- a/common/Errors.v
+++ b/common/Errors.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Events.v b/common/Events.v
index aae0662c..c4a6e7f9 100644
--- a/common/Events.v
+++ b/common/Events.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index a83f2caf..4c9e7889 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Linking.v b/common/Linking.v
index a5cf0a4a..089f4fd2 100644
--- a/common/Linking.v
+++ b/common/Linking.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Memdata.v b/common/Memdata.v
index 411cbc58..1bd87169 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Memory.v b/common/Memory.v
index b16a98b6..fa60455b 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -9,10 +9,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Memtype.v b/common/Memtype.v
index 1d6f252b..b8ad1a6b 100644
--- a/common/Memtype.v
+++ b/common/Memtype.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index cf3a17d5..61c76c91 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Sections.ml b/common/Sections.ml
index 9858f957..794b8470 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Sections.mli b/common/Sections.mli
index a3dad3be..8ec98e40 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Separation.v b/common/Separation.v
index dcd07ca8..f41d94c3 100644
--- a/common/Separation.v
+++ b/common/Separation.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 5ac67c96..f337ba3c 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Subtyping.v b/common/Subtyping.v
index f1047d45..8e5d9361 100644
--- a/common/Subtyping.v
+++ b/common/Subtyping.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Switch.v b/common/Switch.v
index 748aa459..b9aeed96 100644
--- a/common/Switch.v
+++ b/common/Switch.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Switchaux.ml b/common/Switchaux.ml
index 4035e299..47ded8ee 100644
--- a/common/Switchaux.ml
+++ b/common/Switchaux.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Unityping.v b/common/Unityping.v
index 6dbd3c48..1089b359 100644
--- a/common/Unityping.v
+++ b/common/Unityping.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/common/Values.v b/common/Values.v
index f8a666c0..891c9a88 100644
--- a/common/Values.v
+++ b/common/Values.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/configure b/configure
index 9b00e1be..b342b143 100755
--- a/configure
+++ b/configure
@@ -8,10 +8,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.                            #
 #                                                                     #
 #######################################################################
 
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 6d4050f1..ad6e1696 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Bitfields.mli b/cparser/Bitfields.mli
index 45899a46..3ac42495 100644
--- a/cparser/Bitfields.mli
+++ b/cparser/Bitfields.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/C.mli b/cparser/C.mli
index 15717565..763a9277 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index ff046cba..accb95a0 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml
index 7cffef08..36f67283 100644
--- a/cparser/Cabshelper.ml
+++ b/cparser/Cabshelper.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index ecf83779..14f61e06 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Ceval.mli b/cparser/Ceval.mli
index 32a0ed91..5b9bb0d7 100644
--- a/cparser/Ceval.mli
+++ b/cparser/Ceval.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cflow.ml b/cparser/Cflow.ml
index 8a2a3fe4..061e958e 100644
--- a/cparser/Cflow.ml
+++ b/cparser/Cflow.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cflow.mli b/cparser/Cflow.mli
index 0de245ae..8348b37e 100644
--- a/cparser/Cflow.mli
+++ b/cparser/Cflow.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Checks.ml b/cparser/Checks.ml
index 17caf19a..507488f2 100644
--- a/cparser/Checks.ml
+++ b/cparser/Checks.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Checks.mli b/cparser/Checks.mli
index cfd7b04d..08ce4e9a 100644
--- a/cparser/Checks.mli
+++ b/cparser/Checks.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 63ac8ac1..62b00e04 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cleanup.mli b/cparser/Cleanup.mli
index 818a51bc..c469936a 100644
--- a/cparser/Cleanup.mli
+++ b/cparser/Cleanup.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 9aeec421..93377989 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index be7ce029..01175d36 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 3467c092..2dcf193d 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 2ddee78c..17eb2207 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index 86a5e522..483b0376 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 0f0a0ea5..1210353f 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 05717d97..a5b87e2e 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Elab.mli b/cparser/Elab.mli
index 59c5efc1..bca4f74d 100644
--- a/cparser/Elab.mli
+++ b/cparser/Elab.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 00806be1..7918c31f 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Env.mli b/cparser/Env.mli
index 589a76c7..7c1096cf 100644
--- a/cparser/Env.mli
+++ b/cparser/Env.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/ErrorReports.ml b/cparser/ErrorReports.ml
index e8f0bee5..ac1e17ac 100644
--- a/cparser/ErrorReports.ml
+++ b/cparser/ErrorReports.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/ErrorReports.mli b/cparser/ErrorReports.mli
index dbaba5ff..c2160b49 100644
--- a/cparser/ErrorReports.mli
+++ b/cparser/ErrorReports.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index df2da2a2..d34dd654 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 458e51d3..31385b45 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/GCC.mli b/cparser/GCC.mli
index f26d12df..0163c98e 100644
--- a/cparser/GCC.mli
+++ b/cparser/GCC.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index bce0e504..94e490ca 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 8de4ed07..c47ec594 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index aa99f1aa..f9d347b9 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 4c70c7ae..6bea4b92 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 542ed0d7..d88d439b 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index 433e2e73..c406d96c 100644
--- a/cparser/Parse.mli
+++ b/cparser/Parse.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index 93d84ecf..f1abe3d9 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -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.                            */
 /*                                                                     */
 /* *********************************************************************/
 
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 64412194..96424bf8 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Rename.mli b/cparser/Rename.mli
index 818a51bc..c469936a 100644
--- a/cparser/Rename.mli
+++ b/cparser/Rename.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/StructPassing.ml b/cparser/StructPassing.ml
index 222da367..f1f481d0 100644
--- a/cparser/StructPassing.ml
+++ b/cparser/StructPassing.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/StructPassing.mli b/cparser/StructPassing.mli
index 45899a46..3ac42495 100644
--- a/cparser/StructPassing.mli
+++ b/cparser/StructPassing.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index a57d94c4..2ca235f1 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Transform.mli b/cparser/Transform.mli
index 220b7944..c00fd15c 100644
--- a/cparser/Transform.mli
+++ b/cparser/Transform.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 8530ae01..4b1f2262 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/Unblock.mli b/cparser/Unblock.mli
index e6bea9e4..bd807096 100644
--- a/cparser/Unblock.mli
+++ b/cparser/Unblock.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml
index ee6976d4..e3ab3291 100644
--- a/cparser/deLexer.ml
+++ b/cparser/deLexer.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/handcrafted.messages b/cparser/handcrafted.messages
index 23e90b3e..db7318c4 100644
--- a/cparser/handcrafted.messages
+++ b/cparser/handcrafted.messages
@@ -7,10 +7,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.                            #
 #                                                                     #
 #######################################################################
 
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index 4b62b235..cffbd192 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -7,10 +7,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.                            */
 /*                                                                     */
 /* *********************************************************************/
 
diff --git a/cparser/pre_parser_aux.ml b/cparser/pre_parser_aux.ml
index 4a4953ba..a35305ac 100644
--- a/cparser/pre_parser_aux.ml
+++ b/cparser/pre_parser_aux.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/cparser/pre_parser_aux.mli b/cparser/pre_parser_aux.mli
index f6b98a95..36e33bc5 100644
--- a/cparser/pre_parser_aux.mli
+++ b/cparser/pre_parser_aux.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index f96513d1..708be1cb 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 5e27370e..44c76cc6 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml
index a6158b60..88d44c08 100644
--- a/exportclight/Clightnorm.ml
+++ b/exportclight/Clightnorm.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 3ef2e4d3..474a1bd8 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 521c0cdd..8c2a52a2 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Axioms.v b/lib/Axioms.v
index fdc89920..d7b3d036 100644
--- a/lib/Axioms.v
+++ b/lib/Axioms.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v
index e8c1d831..6479c1ee 100644
--- a/lib/BoolEqual.v
+++ b/lib/BoolEqual.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index af65b28e..8ad1ed39 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Commandline.ml b/lib/Commandline.ml
index 672ed834..2f0d7cc1 100644
--- a/lib/Commandline.ml
+++ b/lib/Commandline.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Commandline.mli b/lib/Commandline.mli
index 8bb6f18f..cb9a7513 100644
--- a/lib/Commandline.mli
+++ b/lib/Commandline.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index e0789078..1e93b91d 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
index 73f080b6..69ba4723 100644
--- a/lib/Decidableplus.v
+++ b/lib/Decidableplus.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v
index f16805c6..936814c1 100644
--- a/lib/FSetAVLplus.v
+++ b/lib/FSetAVLplus.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Floats.v b/lib/Floats.v
index 9d0d1668..f56078aa 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Heaps.v b/lib/Heaps.v
index 85343998..def9da97 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 580d4f90..b0d1944e 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Integers.v b/lib/Integers.v
index 9368b531..b38f8564 100644
--- a/lib/Integers.v
+++ b/lib/Integers.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Intv.v b/lib/Intv.v
index 82d3c751..4b5ed77d 100644
--- a/lib/Intv.v
+++ b/lib/Intv.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/IntvSets.v b/lib/IntvSets.v
index 7250a9f6..c3fda5f7 100644
--- a/lib/IntvSets.v
+++ b/lib/IntvSets.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 0cca7fb7..82110bff 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 85fc03f3..6fed3f21 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Maps.v b/lib/Maps.v
index c617d488..6bc6e14b 100644
--- a/lib/Maps.v
+++ b/lib/Maps.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Ordered.v b/lib/Ordered.v
index 69dc1c69..d02892ce 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Parmov.v b/lib/Parmov.v
index f602bd60..d7cab86a 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -8,10 +8,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Postorder.v b/lib/Postorder.v
index eaeaea37..0be7d0b4 100644
--- a/lib/Postorder.v
+++ b/lib/Postorder.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Printlines.ml b/lib/Printlines.ml
index 453096bc..135672cc 100644
--- a/lib/Printlines.ml
+++ b/lib/Printlines.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Printlines.mli b/lib/Printlines.mli
index 545eb033..ec4a1040 100644
--- a/lib/Printlines.mli
+++ b/lib/Printlines.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Readconfig.mli b/lib/Readconfig.mli
index c81e7786..9e3e03d5 100644
--- a/lib/Readconfig.mli
+++ b/lib/Readconfig.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll
index 8abcc407..9d5b692b 100644
--- a/lib/Readconfig.mll
+++ b/lib/Readconfig.mll
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Responsefile.mli b/lib/Responsefile.mli
index ada5a15d..84a58971 100644
--- a/lib/Responsefile.mli
+++ b/lib/Responsefile.mli
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Responsefile.mll b/lib/Responsefile.mll
index 35a2dbdb..430c6b4e 100644
--- a/lib/Responsefile.mll
+++ b/lib/Responsefile.mll
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Tokenize.mli b/lib/Tokenize.mli
index a9f22c4d..f119dcfa 100644
--- a/lib/Tokenize.mli
+++ b/lib/Tokenize.mli
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Tokenize.mll b/lib/Tokenize.mll
index 70e21d55..bd0f433b 100644
--- a/lib/Tokenize.mll
+++ b/lib/Tokenize.mll
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index c4a2f5b1..67e4271d 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v
index a1e4b4ff..6e52cd36 100644
--- a/lib/Wfsimpl.v
+++ b/lib/Wfsimpl.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/lib/Zbits.v b/lib/Zbits.v
index 0539d04b..f6dc0c9d 100644
--- a/lib/Zbits.v
+++ b/lib/Zbits.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index ae10c54c..28859051 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v
index 9d7aadd9..b3fdebd0 100644
--- a/powerpc/Builtins1.v
+++ b/powerpc/Builtins1.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index e0826877..dc8aa73a 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index 5193e453..202f4436 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 1b24e732..9e561ca8 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v
index 53c83d7e..cd6f8cc4 100644
--- a/riscV/Builtins1.v
+++ b/riscV/Builtins1.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index a2087cb7..9ff4e029 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/riscV/extractionMachdep.v b/riscV/extractionMachdep.v
index c9a1040a..890735ba 100644
--- a/riscV/extractionMachdep.v
+++ b/riscV/extractionMachdep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/tools/modorder.ml b/tools/modorder.ml
index 7ca6a9e9..b72ae762 100644
--- a/tools/modorder.ml
+++ b/tools/modorder.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/tools/ndfun.ml b/tools/ndfun.ml
index b6a87ede..3e3daad2 100644
--- a/tools/ndfun.ml
+++ b/tools/ndfun.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/tools/xtime.ml b/tools/xtime.ml
index fbb25a49..3480f229 100644
--- a/tools/xtime.ml
+++ b/tools/xtime.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/x86/Builtins1.v b/x86/Builtins1.v
index f1d60961..e5233ff5 100644
--- a/x86/Builtins1.v
+++ b/x86/Builtins1.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index a16f3ef7..a549cd25 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index 614ec589..26a3f0a7 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index bbc04950..0a7f365b 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index 0e027c0f..ed6dc317 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -7,10 +7,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.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
-- 
cgit 


From 19e1039a26b01297e19590340d7acb25a49b0560 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 8 May 2021 09:13:44 +0200
Subject: Update Changelog

---
 Changelog | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/Changelog b/Changelog
index bda21a96..2e14d2ca 100644
--- a/Changelog
+++ b/Changelog
@@ -2,6 +2,8 @@ New features:
 - New port: AArch64 (ARM 64 bits, "Apple silicon") under macOS.
 - Support bitfields of types other than `int`, provided they are no larger
   than 32 bits (#387)
+- Support `__builtin_unreachable` and `__builtin_expect` (#394)
+  (but these builtins are not used for optimization yet)
 
 Optimizations:
 - Improved branch tunneling: optimized conditional branches can
@@ -16,7 +18,7 @@ Usability:
 Compiler internals:
 - Finer control of variable initialization in sections.  Now we can
   put variables initialized with symbol addresses that need relocation
-  in specific sections (e.g. `const_data`).
+  in specific sections (e.g. `const_data` on macOS).
 - Support re-normalization of function parameters at function entry,
   as required by the AArch64/ELF ABI.
 - PowerPC 64 bits: remove `Pfcfi`, `Pfcfiu`, `Pfctiu` pseudo-instructions,
@@ -37,6 +39,9 @@ Bug fixing:
   return the correct pointer in register EAX (#377).
 - PowerPC, ARM, AArch64: updated the registers destroyed by asm
   pseudo-instructions and built-in functions.
+- Remove spurious error on initialization of a local struct
+  containing a flexible array member.
+- Fixed bug in emulation of assignment to a volatile bit-field (#395).
 
 The clightgen tool:
 - Move the `$` notation for Clight identifiers to scope `clight_scope`
@@ -50,6 +55,11 @@ Coq development:
 - Use the `lia` tactic instead of `omega`.
 - Updated the Flocq library to version 3.4.0.
 
+Licensing and distribution:
+- Dual-licensed source files are now distributed under the LGPL version 2.1
+  (plus the Inria non-commercial license) instead of the GPL version 2
+  (plus the Inria non-commercial license).
+
 
 Release 3.8, 2020-11-16
 =======================
-- 
cgit 


From b42705f033ff0b70247e13c9589084fd9698ae90 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 9 May 2021 18:08:26 +0200
Subject: Update for release 3.9

Also: limit the max width of the page, to avoid very long lines.
---
 doc/index.html | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/doc/index.html b/doc/index.html
index ec8c4d91..c3912cb2 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -8,6 +8,7 @@
 body {
   color: black; background: white;
   margin-left: 5%; margin-right: 5%;
+  max-width:750px;
 }
 h2 { margin-left: -5%;}
 h3 { margin-left: -3%; }
@@ -24,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.8, 2020-11-16</H3>
+<H3 align="center">Version 3.9, 2021-05-10</H3>
 
 <H2>Introduction</H2>
 
@@ -46,9 +47,9 @@ Journal of Automated Reasoning 43(4):363-446, 2009.
 
 <P>This Web site gives a commented listing of the underlying Coq
 specifications and proofs.  Proof scripts are folded by default, but
-can be viewed by clicking on "Proof".  Some modules (written in <I>italics</I> below) differ between the four target architectures.  The
-PowerPC versions of these modules are shown below; the ARM, x86 and RISC-V
-versions can be found in the source distribution.
+can be viewed by clicking on "Proof".  Some modules (written in <I>italics</I> below) differ between the five target architectures.  The
+PowerPC versions of these modules are shown below; the AArch64, ARM,
+x86 and RISC-V versions can be found in the source distribution.
 </P>
 
 <P> This development is a work in progress; some parts have
-- 
cgit 


From 63ba4b55d198fb6a783256d6759887b31ca3d031 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 9 May 2021 18:10:08 +0200
Subject: Update Changelog for release 3.9

---
 Changelog | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Changelog b/Changelog
index 2e14d2ca..aa57a554 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,6 @@
+Release 3.9, 2021-05-10
+=======================
+
 New features:
 - New port: AArch64 (ARM 64 bits, "Apple silicon") under macOS.
 - Support bitfields of types other than `int`, provided they are no larger
-- 
cgit 


From 7b3bc19117e48d601e392f2db2c135c7df1d8376 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 10 May 2021 10:11:36 +0200
Subject: Update for release 3.9

---
 VERSION | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/VERSION b/VERSION
index d5a86723..51212887 100644
--- a/VERSION
+++ b/VERSION
@@ -1,4 +1,4 @@
-version=3.8
+version=3.9
 buildnr=
 tag=
 branch=
-- 
cgit 


From 39710f78062a4a999c079b58181a58e62b78c30b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 13 May 2021 17:26:05 +0200
Subject: Register X1 is destroyed by some built-in functions

E.g. __builtin_bswap.  Update Asm modeling of builtins accordingly.
---
 riscV/Asm.v         | 2 +-
 riscV/Asmgenproof.v | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/riscV/Asm.v b/riscV/Asm.v
index 7e1b1fc8..a47573a2 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -1080,7 +1080,7 @@ Inductive step: state -> trace -> state -> Prop :=
       rs' = nextinstr
               (set_res res vres
                 (undef_regs (map preg_of (destroyed_by_builtin ef))
-                   (rs#X31 <- Vundef))) ->
+                   (rs #X1 <- Vundef #X31 <- Vundef))) ->
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index ab07d071..798dad9f 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -835,13 +835,15 @@ Local Transparent destroyed_by_op.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
   unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence. 
+  rewrite set_res_other. rewrite undef_regs_other_2.
+  rewrite ! Pregmap.gso by congruence. 
   rewrite <- H1. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   rewrite preg_notin_charact. intros. auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. apply Pregmap.gso; auto with asmgen.
+  eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto.
+  rewrite ! Pregmap.gso; auto with asmgen.
   congruence.
 
 - (* Mgoto *)
-- 
cgit 


From 9eccbd39710aab5d6bfe021c57f50a1916d37f70 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 1 Jun 2021 14:40:30 +0200
Subject: Support `# 0 ...` preprocessed line directive

Before, the line number had to start with a nonzero digit.  However,
the GCC 11 preprocessor was observed to produce `# 0 ...` directives.

Fixes: #398
---
 cparser/Lexer.mll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 94e490ca..42980d30 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -393,7 +393,7 @@ and string_literal startp accu = parse
 (* We assume gcc -E syntax but try to tolerate variations. *)
 and hash = parse
   | whitespace_char_no_newline +
-    (decimal_constant as n)
+    (digit + as n)
     whitespace_char_no_newline *
     "\"" ([^ '\n' '\"']* as file) "\""
     [^ '\n']* '\n'
-- 
cgit