Merge branch 'towards_2.10' of ../towards_3.10 into kvx-work

4 files changed, 0 insertions, 716 deletions

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
deleted file mode 100644
index 708be1cb..00000000
--- a/exportclight/Clightdefs.v
+++ /dev/null
@@ -1,304 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  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.                            *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** All imports and definitions used by .v Clight files generated by clightgen *)
-
-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.
-Definition tshort := Tint I16 Signed noattr.
-Definition tushort := Tint I16 Unsigned noattr.
-Definition tint := Tint I32 Signed noattr.
-Definition tuint := Tint I32 Unsigned noattr.
-Definition tbool := Tint IBool Unsigned noattr.
-Definition tlong := Tlong Signed noattr.
-Definition tulong := Tlong Unsigned noattr.
-Definition tfloat := Tfloat F32 noattr.
-Definition tdouble := Tfloat F64 noattr.
-Definition tptr (t: type) := Tpointer t noattr.
-Definition tarray (t: type) (sz: Z) := Tarray t sz noattr.
-
-Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}.
-
-Definition tattr (a: attr) (ty: type) :=
-  match ty with
-  | Tvoid => Tvoid
-  | Tint sz si _ => Tint sz si a
-  | Tlong si _ => Tlong si a
-  | Tfloat sz _ => Tfloat sz a
-  | Tpointer elt _ => Tpointer elt a
-  | Tarray elt sz _ => Tarray elt sz a
-  | Tfunction args res cc => Tfunction args res cc
-  | Tstruct id _ => Tstruct id a
-  | Tunion id  _ => Tunion id a
-  end.
-
-Definition tvolatile (ty: type) := tattr volatile_attr ty.
-
-Definition talignas (n: N) (ty: type) :=
-  tattr {| attr_volatile := false; attr_alignas := Some n |} ty.
-
-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.
-
-Definition build_composite_env' (types: list composite_definition)
-                                (WF: wf_composites types)
-                             : { ce | build_composite_env types  = OK ce }.
-Proof.
-  revert WF. unfold wf_composites. case (build_composite_env types); intros.
-- exists c; reflexivity.
-- contradiction.
-Defined.
-
-Definition mkprogram (types: list composite_definition)
-                     (defs: list (ident * globdef fundef type))
-                     (public: list ident)
-                     (main: ident)
-                     (WF: wf_composites types) : Clight.program :=
-  let (ce, EQ) := build_composite_env' types WF in
-  {| prog_defs := defs;
-     prog_public := public;
-     prog_main := main;
-     prog_types := types;
-     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]. *)
-
-Definition append_bit_pos (b: bool) (p: positive) : positive :=
-  if b then xI p else xO p.
-
-Definition append_char_pos_default (c: ascii) (p: positive) : positive :=
-  let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in
-  xI (xI (xI (xI (xI (xI
-    (append_bit_pos b0 (append_bit_pos b1
-    (append_bit_pos b2 (append_bit_pos b3
-    (append_bit_pos b4 (append_bit_pos b5
-    (append_bit_pos b6 (append_bit_pos b7 p))))))))))))).
-
-Definition append_char_pos (c: ascii) (p: positive) : positive :=
-  match c with
-  | "0"%char => xO (xO (xO (xO (xO (xO p)))))
-  | "1"%char => xI (xO (xO (xO (xO (xO p)))))
-  | "2"%char => xO (xI (xO (xO (xO (xO p)))))
-  | "3"%char => xI (xI (xO (xO (xO (xO p)))))
-  | "4"%char => xO (xO (xI (xO (xO (xO p)))))
-  | "5"%char => xI (xO (xI (xO (xO (xO p)))))
-  | "6"%char => xO (xI (xI (xO (xO (xO p)))))
-  | "7"%char => xI (xI (xI (xO (xO (xO p)))))
-  | "8"%char => xO (xO (xO (xI (xO (xO p)))))
-  | "9"%char => xI (xO (xO (xI (xO (xO p)))))
-  | "a"%char => xO (xI (xO (xI (xO (xO p)))))
-  | "b"%char => xI (xI (xO (xI (xO (xO p)))))
-  | "c"%char => xO (xO (xI (xI (xO (xO p)))))
-  | "d"%char => xI (xO (xI (xI (xO (xO p)))))
-  | "e"%char => xO (xI (xI (xI (xO (xO p)))))
-  | "f"%char => xI (xI (xI (xI (xO (xO p)))))
-  | "g"%char => xO (xO (xO (xO (xI (xO p)))))
-  | "h"%char => xI (xO (xO (xO (xI (xO p)))))
-  | "i"%char => xO (xI (xO (xO (xI (xO p)))))
-  | "j"%char => xI (xI (xO (xO (xI (xO p)))))
-  | "k"%char => xO (xO (xI (xO (xI (xO p)))))
-  | "l"%char => xI (xO (xI (xO (xI (xO p)))))
-  | "m"%char => xO (xI (xI (xO (xI (xO p)))))
-  | "n"%char => xI (xI (xI (xO (xI (xO p)))))
-  | "o"%char => xO (xO (xO (xI (xI (xO p)))))
-  | "p"%char => xI (xO (xO (xI (xI (xO p)))))
-  | "q"%char => xO (xI (xO (xI (xI (xO p)))))
-  | "r"%char => xI (xI (xO (xI (xI (xO p)))))
-  | "s"%char => xO (xO (xI (xI (xI (xO p)))))
-  | "t"%char => xI (xO (xI (xI (xI (xO p)))))
-  | "u"%char => xO (xI (xI (xI (xI (xO p)))))
-  | "v"%char => xI (xI (xI (xI (xI (xO p)))))
-  | "w"%char => xO (xO (xO (xO (xO (xI p)))))
-  | "x"%char => xI (xO (xO (xO (xO (xI p)))))
-  | "y"%char => xO (xI (xO (xO (xO (xI p)))))
-  | "z"%char => xI (xI (xO (xO (xO (xI p)))))
-  | "A"%char => xO (xO (xI (xO (xO (xI p)))))
-  | "B"%char => xI (xO (xI (xO (xO (xI p)))))
-  | "C"%char => xO (xI (xI (xO (xO (xI p)))))
-  | "D"%char => xI (xI (xI (xO (xO (xI p)))))
-  | "E"%char => xO (xO (xO (xI (xO (xI p)))))
-  | "F"%char => xI (xO (xO (xI (xO (xI p)))))
-  | "G"%char => xO (xI (xO (xI (xO (xI p)))))
-  | "H"%char => xI (xI (xO (xI (xO (xI p)))))
-  | "I"%char => xO (xO (xI (xI (xO (xI p)))))
-  | "J"%char => xI (xO (xI (xI (xO (xI p)))))
-  | "K"%char => xO (xI (xI (xI (xO (xI p)))))
-  | "L"%char => xI (xI (xI (xI (xO (xI p)))))
-  | "M"%char => xO (xO (xO (xO (xI (xI p)))))
-  | "N"%char => xI (xO (xO (xO (xI (xI p)))))
-  | "O"%char => xO (xI (xO (xO (xI (xI p)))))
-  | "P"%char => xI (xI (xO (xO (xI (xI p)))))
-  | "Q"%char => xO (xO (xI (xO (xI (xI p)))))
-  | "R"%char => xI (xO (xI (xO (xI (xI p)))))
-  | "S"%char => xO (xI (xI (xO (xI (xI p)))))
-  | "T"%char => xI (xI (xI (xO (xI (xI p)))))
-  | "U"%char => xO (xO (xO (xI (xI (xI p)))))
-  | "V"%char => xI (xO (xO (xI (xI (xI p)))))
-  | "W"%char => xO (xI (xO (xI (xI (xI p)))))
-  | "X"%char => xI (xI (xO (xI (xI (xI p)))))
-  | "Y"%char => xO (xO (xI (xI (xI (xI p)))))
-  | "Z"%char => xI (xO (xI (xI (xI (xI p)))))
-  | "_"%char => xO (xI (xI (xI (xI (xI p)))))
-  | _ => append_char_pos_default c p
-  end.
-
-Fixpoint ident_of_string (s: string) : ident :=
-  match s with
-  | EmptyString => xH
-  | String c s => append_char_pos c (ident_of_string s)
-  end.
-
-(** The inverse conversion, from encoded strings to strings *)
-
-Section DECODE_BITS.
-
-Variable rec: positive -> string.
-
-Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string :=
-  match n with
-  | O => 
-      match l with 
-      | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ =>
-          String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p)
-      | _ => EmptyString
-      end
-  | S n =>
-      match p with
-      | xO q => decode_n_bits n (false :: l) q
-      | xI q => decode_n_bits n (true :: l) q
-      | xH => EmptyString
-      end
-  end.
-
-Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil).
-
-End DECODE_BITS.
-
-Fixpoint string_of_ident (p: positive) : string :=
-  match p with
-  | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p)
-  | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p)
-  | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p)
-  | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p)
-  | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p)
-  | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p)
-  | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p)
-  | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p)
-  | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p)
-  | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p)
-  | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p)
-  | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p)
-  | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p)
-  | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p)
-  | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p)
-  | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p)
-  | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p)
-  | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p)
-  | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p)
-  | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p)
-  | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p)
-  | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p)
-  | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p)
-  | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p)
-  | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p)
-  | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p)
-  | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p)
-  | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p)
-  | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p)
-  | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p)
-  | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p)
-  | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p)
-  | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p)
-  | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p)
-  | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p)
-  | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p)
-  | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p)
-  | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p)
-  | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p)
-  | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p)
-  | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p)
-  | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p)
-  | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p)
-  | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p)
-  | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p)
-  | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p)
-  | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p)
-  | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p)
-  | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p)
-  | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p)
-  | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p)
-  | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p)
-  | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p)
-  | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p)
-  | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p)
-  | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p)
-  | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p)
-  | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p)
-  | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p)
-  | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p)
-  | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p)
-  | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p)
-  | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p)
-  | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p
-  | _ => EmptyString
-  end.
-
-Lemma string_of_ident_of_string:
-  forall s, string_of_ident (ident_of_string s) = s.
-Proof.
-  induction s as [ | c s]; simpl.
-- auto.
-- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity.
-Qed.
-
-Corollary ident_of_string_injective:
-  forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2.
-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.
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
deleted file mode 100644
index 44c76cc6..00000000
--- a/exportclight/Clightgen.ml
+++ /dev/null
@@ -1,201 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  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.                            *)
-(*                                                                     *)
-(* *********************************************************************)
-
-open Printf
-open Commandline
-open Clflags
-open CommonOptions
-open Driveraux
-open Frontend
-open Diagnostics
-
-let tool_name = "Clight generator"
-
-(* clightgen-specific options *)
-
-let option_normalize = ref false
-
-(* From CompCert C AST to Clight *)
-
-let compile_c_ast sourcename csyntax ofile =
-  let loc = file_loc sourcename in
-  let clight =
-    match SimplExpr.transl_program csyntax with
-    | Errors.OK p ->
-        begin match SimplLocals.transf_program p with
-        | Errors.OK p' ->
-            if !option_normalize
-            then Clightnorm.norm_program p'
-            else p'
-        | Errors.Error msg ->
-          fatal_error loc "%a" print_error  msg
-        end
-    | Errors.Error msg ->
-      fatal_error loc "%a" print_error msg in
-  (* Dump Clight in C syntax if requested *)
-  PrintClight.print_if_2 clight;
-  (* Print Clight in Coq syntax *)
-  let oc = open_out ofile in
-  ExportClight.print_program (Format.formatter_of_out_channel oc)
-                             clight sourcename !option_normalize;
-  close_out oc
-
-(* From C source to Clight *)
-
-let compile_c_file sourcename ifile ofile =
-  let set_dest dst opt ext =
-    dst := if !opt then Some (output_filename sourcename ".c" ext)
-      else None in
-  set_dest Cprint.destination option_dparse ".parsed.c";
-  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
-  set_dest PrintClight.destination option_dclight ".light.c";
-  compile_c_ast sourcename (parse_c_file sourcename ifile) ofile
-
-let output_filename sourcename suff =
-  let prefixname = Filename.chop_suffix sourcename suff in
-  output_filename_default (prefixname ^ ".v")
-
-(* Processing of a .c file *)
-
-let process_c_file sourcename =
-  ensure_inputfile_exists sourcename;
-  let ofile = output_filename sourcename ".c" in
-  if !option_E then begin
-    preprocess sourcename "-"
-  end else begin
-    let preproname = if !option_dprepro then
-        Driveraux.output_filename sourcename ".c" ".i"
-      else
-        Driveraux.tmp_file ".i" in
-    preprocess sourcename preproname;
-    compile_c_file sourcename preproname ofile
-  end
-
-(* Processing of a .i file *)
-
-let process_i_file sourcename =
-  ensure_inputfile_exists sourcename;
-  let ofile = output_filename sourcename ".i" in
-  compile_c_file sourcename sourcename ofile
-
-let usage_string =
-  version_string tool_name ^
-{|Usage: clightgen [options] <source files>
-Recognized source files:
-  .c             C source file
-  .i or .p       C source file that should not be preprocessed
-Processing options:
-  -normalize     Normalize the generated Clight code w.r.t. loads in expressions
-  -canonical-idents  Use canonical numbers to represent identifiers  (default)
-  -short-idents  Use small, non-canonical numbers to represent identifiers
-  -E             Preprocess only, send result to standard output
-  -o <file>      Generate output in <file>
-|} ^
-prepro_help ^
-language_support_help ^
-{|Tracing options:
-  -dprepro       Save C file after preprocessing in <file>.i
-  -dparse        Save C file after parsing and elaboration in <file>.parsed.c
-  -dc            Save generated Compcert C in <file>.compcert.c
-  -dclight       Save generated Clight in <file>.light.c
-  -dall          Save all generated intermediate files in <file>.<ext>
-|} ^
-  general_help ^
-  warning_help
-
-
-let print_usage_and_exit () =
-  printf "%s" usage_string; exit 0
-
-let set_all opts () = List.iter (fun r -> r := true) opts
-let unset_all opts () = List.iter (fun r -> r := false) opts
-
-let actions : ((string -> unit) * string) list ref = ref []
-let push_action fn arg =
-  actions := (fn, arg) :: !actions
-
-let perform_actions () =
-  let rec perform = function
-    | [] -> ()
-    | (fn,arg) :: rem -> fn arg; perform rem
-  in perform (List.rev !actions)
-
-let num_input_files = ref 0
-
-let cmdline_actions =
-  [
-(* Getting help *)
-  Exact "-help", Unit print_usage_and_exit;
-  Exact "--help", Unit print_usage_and_exit;]
-  (* Getting version info *)
- @ version_options tool_name @
-(* Processing options *)
- [ Exact "-E", Set option_E;
-  Exact "-normalize", Set option_normalize;
-  Exact "-canonical-idents", Set Camlcoq.use_canonical_atoms;
-  Exact "-short-idents", Unset Camlcoq.use_canonical_atoms;
-  Exact "-o", String(fun s -> option_o := Some s);
-  Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
-                              option_o := Some s);]
-(* Preprocessing options *)
-  @ prepro_actions @
-(* Tracing options *)
-  [ Exact "-dprepro", Set option_dprepro;
-   Exact "-dparse", Set option_dparse;
-   Exact "-dc", Set option_dcmedium;
-   Exact "-dclight", Set option_dclight;
-   Exact "-dall", Self (fun _ ->
-       option_dprepro := true;
-       option_dparse := true;
-       option_dcmedium := true;
-       option_dclight := true;);
- ]
-  @ general_options
-(* Diagnostic options *)
-  @ warning_options
-  @ language_support_options @
-(* Catch options that are not handled *)
-  [Prefix "-", Self (fun s ->
-     fatal_error no_loc "Unknown option `%s'" s);
-(* File arguments *)
-  Suffix ".c", Self (fun s ->
-      incr num_input_files; push_action process_c_file s);
-  Suffix ".i", Self (fun s ->
-      incr num_input_files; push_action process_i_file s);
-  Suffix ".p", Self (fun s ->
-      incr num_input_files; push_action process_i_file s);
-  ]
-
-let _ =
-try
-  Gc.set { (Gc.get()) with
-              Gc.minor_heap_size = 524288; (* 512k *)
-              Gc.major_heap_increment = 4194304 (* 4M *)
-         };
-  Printexc.record_backtrace true;
-  Camlcoq.use_canonical_atoms := true;
-  Frontend.init ();
-  parse_cmdline cmdline_actions;
-  if !option_o <> None && !num_input_files >= 2 then
-    fatal_error no_loc "Ambiguous '-o' option (multiple source files)";
-  if !num_input_files = 0 then
-    fatal_error no_loc "no input file";
-  perform_actions ()
-with
-  | Sys_error msg
-  | CmdError msg -> error no_loc "%s" msg; exit 2
-  | Abort -> exit 2
-  | e -> crash e
diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml
deleted file mode 100644
index 88d44c08..00000000
--- a/exportclight/Clightnorm.ml
+++ /dev/null
@@ -1,178 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  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.                            *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Clight-to-Clight rewriting to name memory loads *)
-
-(* The effect of this rewriting is to ensure that Clight expressions
-  whose evaluation involves a memory load (i.e. a lvalue-to-rvalue
-  conversion with By_value access mode) are always bound to a temporary
-  and never occur deep inside another expression.  For example,
-
-      tmp = *(x + 0) + *(x + 1)
-
-  in the original Clight is rewritten to
-
-      tmp1 = *(x + 0)
-      tmp2 = *(x + 1)
-      tmp = tmp1 + tmp2
-*)
-
-open Camlcoq
-open Ctypes
-open Clight
-
-let gen_next : AST.ident ref = ref P.one
-let gen_trail : (AST.ident * coq_type) list ref = ref []
-
-let gensym ty =
-  let id = !gen_next in
-  gen_next := P.succ id;
-  gen_trail := (id, ty) :: !gen_trail;
-  id
-
-let is_lvalue = function
-  | Evar _ | Ederef _ | Efield _ -> true
-  | _ -> false
-
-let accesses_memory e =
-  is_lvalue e &&
-  match access_mode (typeof e) with By_value _ -> true | _ -> false
-
-(** Normalization of an expression.  Return a normalized expression
-  and a list of statements to be executed before evaluating the expression. *)
-
-let rec norm_expr e =
-  let (sl, e') = norm_expr_1 e in
-  if accesses_memory e then begin
-    let ty = typeof e in
-    let id = gensym ty in
-    (sl @ [Sset(id, e')], Etempvar(id, ty))
-  end else
-    (sl, e')
-
-and norm_expr_1 e =
-  match e with
-  | Econst_int _ | Econst_float _ | Econst_single _ | Econst_long _ -> ([], e)
-  | Evar _ | Etempvar _ -> ([], e)
-  | Ederef(e1, t) ->
-      let (sl, e1') = norm_expr e1 in (sl, Ederef(e1', t))
-  | Eaddrof(e1, t) ->
-      let (sl, e1') = norm_expr_lvalue e1 in (sl, Eaddrof(e1', t))
-  | Eunop(op, e1, t) ->
-      let (sl, e1') = norm_expr e1 in (sl, Eunop(op, e1', t))
-  | Ebinop(op, e1, e2, t) ->
-      let (sl1, e1') = norm_expr e1 in
-      let (sl2, e2') = norm_expr e2 in
-      (sl1 @ sl2, Ebinop(op, e1', e2', t))
-  | Ecast(e1, t) ->
-      let (sl, e1') = norm_expr e1 in (sl, Ecast(e1', t))
-  | Efield(e1, id, t) ->
-      let (sl, e1') = norm_expr e1 in (sl, Efield(e1', id, t))
-  | Esizeof _ | Ealignof _ -> ([], e)
-
-(** An expression in l-value position has no memory dereference at top level,
-  by definition of l-values.  Hence, use the [norm_expr_1] variant.. *)
-and norm_expr_lvalue e = norm_expr_1 e
-
-(** In a [Sset id e] statement, the [e] expression can contain a memory
-  dereference at top level.  Hence, use the [norm_expr_1] variant. *)
-let norm_expr_set_top = norm_expr_1
-
-let rec norm_expr_list el =
-  match el with
-  | [] -> ([], [])
-  | e1 :: el ->
-      let (sl1, e1') = norm_expr e1 in
-      let (sl2, el') = norm_expr_list el in
-      (sl1 @ sl2, e1' :: el')
-
-let rec add_sequence sl s =
-  match sl with
-  | [] -> s
-  | s1 :: sl -> Ssequence(s1, add_sequence sl s)
-
-let rec norm_stmt s =
-  match s with
-  | Sskip -> s
-  | Sassign(e1, e2) ->
-      let (sl1, e1') = norm_expr_lvalue e1 in
-      let (sl2, e2') = norm_expr e2 in
-      add_sequence (sl1 @ sl2) (Sassign(e1', e2'))
-  | Sset(id, e) ->
-      let (sl, e') = norm_expr_set_top e in
-      add_sequence sl (Sset(id, e'))
-  | Scall(optid, e, el) ->
-      let (sl1, e') = norm_expr e in
-      let (sl2, el') = norm_expr_list el in
-      add_sequence (sl1 @ sl2) (Scall(optid, e', el'))  
-  | Sbuiltin(optid, ef, tyl, el) ->
-      let (sl, el') = norm_expr_list el in
-      add_sequence sl (Sbuiltin(optid, ef, tyl, el'))
-  | Ssequence(s1, s2) ->
-      Ssequence(norm_stmt s1, norm_stmt s2)
-  | Sifthenelse(e, s1, s2) ->
-      let (sl, e') = norm_expr e in
-      add_sequence sl (Sifthenelse(e', norm_stmt s1, norm_stmt s2))
-  | Sloop(s1, s2) ->
-      Sloop(norm_stmt s1, norm_stmt s2)
-  | Sbreak | Scontinue | Sreturn None -> s
-  | Sreturn (Some e) ->
-      let (sl, e') = norm_expr e in
-      add_sequence sl (Sreturn(Some e'))
-  | Sswitch(e, ls) ->
-      let (sl, e') = norm_expr e in
-      add_sequence sl (Sswitch(e', norm_lbl_stmt ls))
-  | Slabel(lbl, s1) ->
-      Slabel(lbl, norm_stmt s1)
-  | Sgoto lbl -> s
-
-and norm_lbl_stmt ls =
-  match ls with
-  | LSnil -> LSnil
-  | LScons(n, s, ls) -> LScons(n, norm_stmt s, norm_lbl_stmt ls)
-
-(* In "canonical atoms" mode, temporaries are between 2^7 and 2^12 - 1.
-   Below 2^7 are single-letter identifiers and above 2^12 are all
-   other identifiers. *)
-
-let first_temp = P.of_int 128
-let last_temp  = P.of_int 4095
-
-let next_var curr (v, _) =
-  if P.lt v curr
-  || !use_canonical_atoms && (P.lt v first_temp || P.gt v last_temp)
-  then curr
-  else P.succ v
-
-let next_var_list vars start = List.fold_left next_var start vars
-
-let norm_function f =
-  gen_next := next_var_list f.fn_params
-                (next_var_list f.fn_vars
-                   (next_var_list f.fn_temps
-                     (Camlcoq.first_unused_ident ())));
-  gen_trail := [];
-  let s' = norm_stmt f.fn_body in
-  let new_temps = !gen_trail in
-  { f with fn_body = s'; fn_temps = f.fn_temps @ new_temps }
-
-let norm_fundef = function
-  | Internal f -> Internal (norm_function f)
-  | External _ as fd -> fd
-
-let norm_program p =
-  let p1 = AST.transform_program norm_fundef (program_of_program p) in
-  { p with prog_defs = p1.AST.prog_defs }
diff --git a/exportclight/README.md b/exportclight/README.md
deleted file mode 100644
index 85e0790b..00000000
--- a/exportclight/README.md
+++ /dev/null
@@ -1,33 +0,0 @@
-# The clightgen tool
-
-
-## Overview
-"clightgen" is an experimental tool that transforms C source files
-into Clight abstract syntax, pretty-printed in Coq format in .v files.
-These generated .v files can be loaded in a Coq session for
-interactive verification, typically.
-
-
-## How to build
-
-Change to the top-level CompCert directory and issue
-```
-   make clightgen
-```
-
-## Usage
-```
-   clightgen [options] <C source files>
-```
-For each source file `src.c`, its Clight abstract syntax is generated
-in `src.v`.
-
-The options recognized are a subset of those of the CompCert compiler ccomp
-(see [user's manual](http://compcert.inria.fr/man/manual003.html) for full documentation):
-```
-   -I<dir>     search <dir> for include files
-   -D<symbol>  define preprocessor macro
-   -U<symbol>  undefine preprocessor macro
-   -Wp,<opts>  pass options to C preprocessor
-   -f<feature> activate emulation of the given C feature
-```