parameterize the metalib by the ATOM implementation

Fsub/Fsub_LetSum_Definitions.v

@@ -17,7 +17,7 @@
 *)
 
 Require Export Metalib.Metatheory.
-
+Export Metatheory.AtomMetatheory.
 
 (* ********************************************************************** *)
 (** * #<a name="syntax"></a># Syntax (pre-terms) *)

Metalib/LibLNgen.v

@@ -10,6 +10,7 @@
 Require Export Metalib.LibDefaultSimp.
 Require Import Metalib.Metatheory.
 Require Import Omega.
+Import Metatheory.AtomMetatheory.
 
 
 (* ********************************************************************** *)

Metalib/Metatheory.v

@@ -15,7 +15,11 @@ Require Export Metalib.CoqListFacts.
 Require Export Metalib.LibTactics.
 Require Export Metalib.MetatheoryAtom.
 
+Module Metatheory(Atom : ATOM).
 
+Module AtomLib := ATOMLib(Atom).
+Export AtomLib.  
+
 (* ********************************************************************** *)
 (** * Notations for finite sets of atoms *)
 
@@ -236,7 +240,7 @@ Hint Resolve
 
 (* SCW: this export must be at the end of the file so that eq_dec refers to
    the type class member, not KeySetFacts.eq_dec. *)
-Require Export Metalib.CoqEqDec.
+Export Metalib.CoqEqDec.
 
 (** We prefer that "==" refer to decidable equality at [eq], as
     defined by the [EqDec_eq] class from the CoqEqDec library. *)
@@ -295,3 +299,6 @@ Ltac apply_fresh_base H gather_vars atom_name :=
 Set Implicit Arguments.
 Definition union_map (A:Set) (f:A -> vars) (l:list A) :=
  (List.fold_right (fun t acc => f t \u acc) {}) l.
+End Metatheory.
+
+Module AtomMetatheory := Metatheory(Atom).

Metalib/MetatheoryAtom.v

@@ -108,6 +108,9 @@ Module Atom : ATOM.
 
 End Atom.
 
+Module ATOMLib(Atom : ATOM).
+
+
 (** We make [atom], [fresh], [fresh_not_in] and [atom_fresh_for_list] available
     without qualification. *)
 
@@ -284,3 +287,4 @@ Proof.
   trivial.
 Qed.
 (* end show *)
+End ATOMLib.

Stlc/Connect.v

@@ -27,7 +27,7 @@
  *)
 
 Require Import Metalib.Metatheory.
-
+Import Metatheory.AtomMetatheory.
 Require Import Stlc.Definitions.
 Require Import Stlc.Lemmas.
 

Stlc/Definitions.v

@@ -13,6 +13,7 @@
 
 
 Require Import Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 
 (*************************************************************************)
 (** * Syntax of STLC *)

Stlc/Lec1.v

@@ -129,6 +129,7 @@ version of that output. (For comparison, the raw output is in [Stlc_inf.v].)
     This command will only succeed if you have already run [make] and [make
     install] in the Metatheory directory to compile the Metatheory library. *)
 Require Import Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 
 (** Next, we import the definitions of the simply-typed lambda calculus.
     If you haven't skimmed this file yet, you should do so now. You don't

Stlc/Lec2.v

@@ -5,6 +5,7 @@
 (*************************************************************************)
 
 Require Import Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 Require Import Stlc.Definitions.
 Import StlcNotations.
 

Stlc/Lemmas.v

@@ -2,6 +2,7 @@ Require Import Coq.Logic.FunctionalExtensionality.
 Require Import Coq.Program.Equality.
 
 Require Export Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 Require Export Metalib.LibLNgen.
 
 Require Export Stlc.Definitions.

Stlc/Makefile

@@ -1,6 +1,6 @@
 RULESFILE = stlc-rules.tex
 
-GENCOQ = Stlc.v Stlc_inf.v Lec1_sol.v Lec1_full.v  Lec2_sol.v Lec2_full.v Nominal_full.v Nominal_sol.v Connect_full.v Connect_sol.v
+GENCOQ = Lec1_sol.v Lec1_full.v  Lec2_sol.v Lec2_full.v Nominal_full.v Nominal_sol.v Connect_full.v Connect_sol.v
 
 FULL    = Lec1 Lec2 Nominal Connect
 EXTRA   = Stlc.v Stlc_inf.v stlc.ott stlc.mng ottalt.sty listproc.sty stlc.pdf gen.mk
@@ -34,6 +34,7 @@ zipclean:
 
 clean: Stlc.mk paperclean zipclean
 	make -f Stlc.mk clean
+	rm -f $(GENCOQ)
 	rm -f Stlc.mk
 	rm -f *.cmi *.cmo coqsplit
 

Stlc/Nominal.v

@@ -18,6 +18,7 @@ Require Export Omega.
 (** We will use the [atom] type from the metatheory library to
     represent variable names. *)
 Require Export Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 
 (** Although we are not using LNgen, some of the tactics from
     its library are useful for automating reasoning about

Stlc/Stlc.v

@@ -1,4 +1,5 @@
 Require Import Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 (** syntax *)
 Definition index := nat.
 

Stlc/Stlc_inf.v

@@ -2,6 +2,7 @@ Require Import Coq.Logic.FunctionalExtensionality.
 Require Import Coq.Program.Equality.
 
 Require Export Metalib.Metatheory.
+Import Metatheory.AtomMetatheory.
 Require Export Metalib.LibLNgen.
 
 Require Export Stlc.

Stlc/coqsplit.ml

@@ -292,9 +292,9 @@ let spec =
 
 let readchan chan =
   let nbytes = in_channel_length chan in
-  let string = String.create nbytes in
+  let string = Bytes.create nbytes in
   really_input chan string 0 nbytes;
-  string
+  Bytes.to_string string
 
 let findsubstring s1 s2 =
   let l1 = String.length s1 in

Tutorial/STLC.v

@@ -57,7 +57,7 @@
 *)
 
 Require Import Metalib.Metatheory.
-
+Import Metatheory.AtomMetatheory.
 
 (*************************************************************************)
 (** * Syntax of STLC *)

Tutorial/STLCsol.v

@@ -57,7 +57,7 @@
 *)
 
 Require Import Metalib.Metatheory.
-
+Import Metatheory.AtomMetatheory.
 
 (*************************************************************************)
 (** * Syntax of STLC *)