diff --git a/.gitignore b/.gitignore
index fcb275d..4633a6a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,6 @@
 /*.vo
 /*.glob
 /.*.aux
+/*.v.d
+CoqSrc.mk
+_CoqProject
diff --git a/AssocList.v b/AssocList.v
index e010dba..25946ba 100644
--- a/AssocList.v
+++ b/AssocList.v
@@ -20,9 +20,9 @@ Require Import Coq.FSets.FSets.
 Require Import Coq.Lists.List.
 Require Import Coq.Logic.Decidable.
 
-Require Import CoqFSetDecide.
-Require Import CoqListFacts.
-Require Import LibTactics.
+Require Import Metalib.CoqFSetDecide.
+Require Import Metalib.CoqListFacts.
+Require Import Metalib.LibTactics.
 
 
 (* *********************************************************************** *)
@@ -635,7 +635,7 @@ Section BindsProperties.
     binds x a (y ~ b) ->
     x = y.
   Proof.
-    clear. intros H. inversion H as [HEq | HIn]. 
+    clear. intros H. inversion H as [HEq | HIn].
       inversion HEq; intuition.
       inversion HIn.
   Qed.
diff --git a/AssumeList.v b/AssumeList.v
index 50bbb54..bdfd64e 100644
--- a/AssumeList.v
+++ b/AssumeList.v
@@ -14,13 +14,13 @@ Require Import Coq.FSets.FSets.
 Require Import Coq.Lists.List.
 Require Import Coq.Logic.Decidable.
 
-Require Import CoqFSetDecide.
-Require Import CoqListFacts.
-Require Import LibTactics.
+Require Import Metalib.CoqFSetDecide.
+Require Import Metalib.CoqListFacts.
+Require Import Metalib.LibTactics.
 
-Require Import MetatheoryAtom.
+Require Import Metalib.MetatheoryAtom.
 Import AtomSetImpl.
-Require Import LibTactics.
+Require Import Metalib.LibTactics.
 
 
 (* *********************************************************************** *)
@@ -65,7 +65,7 @@ Require Import LibTactics.
     .
 
     Definition map (f1 : A -> A) (f2: B -> B) (E : list (asn A B)) : list (asn A B) :=
-      List.map (fun x => match x with 
+      List.map (fun x => match x with
                          | VarAsn _ x a => VarAsn B x (f1 a)
                          | AltAsn _ b   => AltAsn A (f2 b)
                          end) E.
@@ -96,17 +96,17 @@ Require Import LibTactics.
           uniq E ->
           x `notin` dom E ->
           uniq ((x ~~ a) ++ E)
-      | uniq_alt : forall b E, 
-          uniq E -> 
+      | uniq_alt : forall b E,
+          uniq E ->
           uniq (one (AltAsn A b) ++ E).
 
     Fixpoint erase (E : list (asn A B)) : list B :=
-      match E with 
+      match E with
       | nil => nil
       | (AltAsn _ b) :: E => b :: erase E
-      | (VarAsn _ x a) :: E => erase E 
+      | (VarAsn _ x a) :: E => erase E
       end.
-     
+
     Unset Implicit Arguments.
   End Definitions.
 
@@ -462,7 +462,7 @@ Require Import LibTactics.
       uniq (E ++ F) -> uniq E.
     Proof.
       clear. intros H; induction E as [ | a E']; simpl_asnlist in *.
-        apply uniq_nil. 
+        apply uniq_nil.
         destruct a.
         apply uniq_push; inversion H; subst.
           auto.
@@ -507,7 +507,7 @@ Require Import LibTactics.
             intuition.
             rewrite disjoint_one_l in Hd. simpl_asnlist. fsetdec.
         apply uniq_alt.
-          inversion HE; subst. 
+          inversion HE; subst.
             intuition.
     Qed.
 
@@ -870,9 +870,9 @@ Require Import LibTactics.
         unfold binds in *. simpl. intros [? | ?].
           destruct a0.
              inversion H; subst.
-             left. congruence. 
+             left. congruence.
              inversion H.
-          destruct a0. 
+          destruct a0.
             right. auto.
             right. auto.
     Qed.
@@ -889,8 +889,8 @@ Require Import LibTactics.
       clear. induction E as [ | y ? F ]; intros J; simpl_asnlist.
       analyze_binds J.
       analyze_binds J; subst; auto with set.
-        inversion H0;subst. simpl. fsetdec. 
-          inversion H.  
+        inversion H0;subst. simpl. fsetdec.
+          inversion H.
     Qed.
 
     Lemma fresh_app_l :
@@ -917,4 +917,3 @@ Require Import LibTactics.
 
 
 
- 
\ No newline at end of file
diff --git a/Attic/MetatheoryEnv.v b/Attic/MetatheoryEnv.v
index 5085597..b2214ab 100644
--- a/Attic/MetatheoryEnv.v
+++ b/Attic/MetatheoryEnv.v
@@ -19,13 +19,13 @@ Require Import Coq.FSets.FSets.
 Require Import Coq.Lists.List.
 Require Import Coq.Logic.Decidable.
 
-Require Import CoqFSetDecide.
-Require Import CoqListFacts.
+Require Import Metalib.CoqFSetDecide.
+Require Import Metalib.CoqListFacts.
 
-Require Import AssocList.
-Require Import MetatheoryAtom.
+Require Import Metalib.AssocList.
+Require Import Metalib.MetatheoryAtom.
 Import AtomSetImpl.
-Require Import LibTactics.
+Require Import Metalib.LibTactics.
 
 
 (* *********************************************************************** *)
diff --git a/Attic/MyAssumeList.v b/Attic/MyAssumeList.v
index 8f10ea0..8fa9514 100644
--- a/Attic/MyAssumeList.v
+++ b/Attic/MyAssumeList.v
@@ -126,6 +126,8 @@ Open Scope list_scope.
 (** [dom] computes the domain of an assumption list, i.e., the
     set consisting of its keys. *)
 
+(* FIXME: commented out by simplicity, but the code should be fixed *)
+(*
 Fixpoint dom
   (A B : Type) (E : list (asn A B))
   : KeySet.t :=
@@ -1552,4 +1554,7 @@ Hint Resolve @binds_weaken.
 
 Hint Immediate @binds_remove_mid @binds_In.
 
+*)
+
 End Make.
+
diff --git a/CoqListFacts.v b/CoqListFacts.v
index 06e2be9..e3f0d72 100644
--- a/CoqListFacts.v
+++ b/CoqListFacts.v
@@ -10,7 +10,7 @@
 Require Import Coq.Lists.List.
 Require Import Coq.Lists.SetoidList.
 
-Require Import CoqUniquenessTac.
+Require Import Metalib.CoqUniquenessTac.
 
 Open Scope list_scope.
 
@@ -126,7 +126,7 @@ Qed.
 
 Lemma InA_iff_In : forall (A : Type) (x : A) (xs : list A),
   InA (@eq _) x xs <-> In x xs.
-Proof. 
+Proof.
   split; auto using InA_In.
   apply SetoidList.In_InA. apply eq_equivalence.
 Qed.
@@ -230,7 +230,7 @@ Section Uniqueness_Of_SetoidList_Proofs.
 
   Theorem lelistA_unique :
     forall (x : A) (xs : list A) (p q : lelistA R x xs), p = q.
-  Proof. induction p using lelistA_ind'; uniqueness 1. Qed. 
+  Proof. induction p using lelistA_ind'; uniqueness 1. Qed.
 
   Theorem sort_unique :
     forall (xs : list A) (p q : sort R xs), p = q.
@@ -238,6 +238,6 @@ Section Uniqueness_Of_SetoidList_Proofs.
 
   Theorem eqlistA_unique :
     forall (xs ys : list A) (p q : eqlistA R xs ys), p = q.
-  Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. 
+  Proof. induction p using eqlistA_ind'; uniqueness 2. Qed.
 
 End Uniqueness_Of_SetoidList_Proofs.
diff --git a/CoqUniquenessTacEx.v b/CoqUniquenessTacEx.v
index f8e0f2f..0ebe7d4 100644
--- a/CoqUniquenessTacEx.v
+++ b/CoqUniquenessTacEx.v
@@ -9,7 +9,7 @@ Require Import Coq.Arith.Peano_dec.
 Require Import Coq.Lists.SetoidList.
 Require Import Coq.omega.Omega.
 
-Require Import CoqUniquenessTac.
+Require Import Metalib.CoqUniquenessTac.
 
 
 (* *********************************************************************** *)
@@ -31,8 +31,8 @@ Proof.
   induction p using le_ind';
   uniqueness 1;
   assert False by omega; intuition.
-  
-Qed. 
+
+Qed.
 
 
 (* ********************************************************************** *)
@@ -64,7 +64,7 @@ Section Uniqueness_Of_SetoidList_Proofs.
 
   Theorem eqlistA_unique :
     forall (xs ys : list A) (p q : eqlistA R xs ys), p = q.
-  Proof. induction p using eqlistA_ind'; uniqueness 2. Qed. 
+  Proof. induction p using eqlistA_ind'; uniqueness 2. Qed.
 
 End Uniqueness_Of_SetoidList_Proofs.
 
diff --git a/FSetExtra.v b/FSetExtra.v
index 6ffa783..eb998a6 100644
--- a/FSetExtra.v
+++ b/FSetExtra.v
@@ -8,7 +8,7 @@
 
 Require Import Coq.FSets.FSets.
 
-Require Import CoqFSetInterface.
+Require Import Metalib.CoqFSetInterface.
 
 
 (* *********************************************************************** *)
diff --git a/FSetWeakNotin.v b/FSetWeakNotin.v
index 33a20ad..1fbd5bf 100644
--- a/FSetWeakNotin.v
+++ b/FSetWeakNotin.v
@@ -14,7 +14,7 @@
 
 Require Import Coq.FSets.FSetInterface.
 
-Require Import CoqFSetDecide.
+Require Import Metalib.CoqFSetDecide.
 
 
 (* *********************************************************************** *)
diff --git a/Fsub_LetSum_Definitions.v b/Fsub_LetSum_Definitions.v
index d7524d2..8bb73f9 100644
--- a/Fsub_LetSum_Definitions.v
+++ b/Fsub_LetSum_Definitions.v
@@ -16,7 +16,7 @@
       - #<a href="##auto">Automation</a>#
 *)
 
-Require Export Metatheory.
+Require Export Metalib.Metatheory.
 
 
 (* ********************************************************************** *)
diff --git a/Fsub_LetSum_Infrastructure.v b/Fsub_LetSum_Infrastructure.v
index 5d50d62..1e7f302 100644
--- a/Fsub_LetSum_Infrastructure.v
+++ b/Fsub_LetSum_Infrastructure.v
@@ -19,7 +19,7 @@
       - #<a href="##auto">Automation</a>#
       - #<a href="##body">Properties of body_e</a># *)
 
-Require Export Fsub_LetSum_Definitions.
+Require Export Metalib.Fsub_LetSum_Definitions.
 
 
 (* ********************************************************************** *)
diff --git a/Fsub_LetSum_Lemmas.v b/Fsub_LetSum_Lemmas.v
index 55209a5..55e70b3 100644
--- a/Fsub_LetSum_Lemmas.v
+++ b/Fsub_LetSum_Lemmas.v
@@ -21,7 +21,7 @@
       - #<a href="##regularity">Regularity lemmas</a>#
       - #<a href="##auto">Automation</a># *)
 
-Require Export Fsub_LetSum_Infrastructure.
+Require Export Metalib.Fsub_LetSum_Infrastructure.
 
 
 (* ********************************************************************** *)
diff --git a/Fsub_LetSum_Soundness.v b/Fsub_LetSum_Soundness.v
index 04f639f..c688be7 100644
--- a/Fsub_LetSum_Soundness.v
+++ b/Fsub_LetSum_Soundness.v
@@ -12,7 +12,7 @@
       - #<a href="##preservation">Preservation</a>#
       - #<a href="##progress">Progress</a># *)
 
-Require Export Fsub_LetSum_Lemmas.
+Require Export Metalib.Fsub_LetSum_Lemmas.
 
 
 (* ********************************************************************** *)
diff --git a/LibLNgen.v b/LibLNgen.v
index 52cfa4e..170bd32 100644
--- a/LibLNgen.v
+++ b/LibLNgen.v
@@ -7,8 +7,8 @@
 
 (** A library of code for supporting LNgen. *)
 
-Require Export LibDefaultSimp.
-Require Import Metatheory.
+Require Export Metalib.LibDefaultSimp.
+Require Import Metalib.Metatheory.
 Require Import Omega.
 
 
diff --git a/Makefile b/Makefile
index d807cdd..bafd6d7 100644
--- a/Makefile
+++ b/Makefile
@@ -25,6 +25,15 @@ COQC = coqc
 COQDEP = coqdep
 COQDOC = coqdoc
 
+
+## Library name used for the imports in Coq
+
+LIBNAME=Metalib
+
+## Name of the submakefile generated by coq_makefile
+
+COQMKFILENAME=CoqSrc.mk
+
 ## Include directories, one per line.
 
 INCDIRS = \
@@ -35,6 +44,7 @@ INCDIRS = \
 DOCDIR = doc/html
 
 ## List of files to be compiled and documented.
+# TODO: should be useless once we get coq_makefile to compile the documentation as well
 
 FILES = \
 	AssocList \
@@ -75,10 +85,17 @@ INCFLAGS = $(foreach i, $(INCDIRS), -I $(i))
 .PHONY: all clean coq dist doc documentation gens
 .SUFFIXES: .v .vo
 
-all: Metatheory.vo MetatheoryAlt.vo LibLNgen.vo
+all: coq # Metatheory.vo MetatheoryAlt.vo LibLNgen.vo
+
+#coq: $(VOFILES)
+coq: $(COQMKFILENAME)
+	# FIXME: loose integration right now, but when the doc works we should be able to simply include the generated makefile
+	@$(MAKE) -f CoqSrc.mk
 
-coq: $(VOFILES)
+$(COQMKFILENAME): Makefile
+	{ echo "-R . $(LIBNAME) " ; ls *.v ; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME)
 
+# TODO: in theory, coq_makefile creates targets for documentation, so we should be able to use it instead of handwritten rules
 doc:
 	+make documentation
 
@@ -87,7 +104,8 @@ documentation: $(DOCDIR) $(VOFILES)
 	cp -f custom.css $(DOCDIR)/coqdoc.css
 
 clean:
-	rm -f *.vo *.glob *.cmi *.cmx *.o
+	#rm -f *.vo *.glob *.cmi *.cmx *.o
+	@$(MAKE) -f CoqSrc.mk clean
 	rm -rf $(DOCDIR)
 
 ############################################################################
diff --git a/Metatheory.v b/Metatheory.v
index 199c0eb..7106b1d 100644
--- a/Metatheory.v
+++ b/Metatheory.v
@@ -10,11 +10,11 @@ Require Export Coq.Arith.Arith.
 Require Export Coq.FSets.FSets.
 Require Export Coq.Lists.List.
 
-Require Export AssocList.
-Require Export CoqEqDec.
-Require Export CoqListFacts.
-Require Export LibTactics.
-Require Export MetatheoryAtom.
+Require Export Metalib.AssocList.
+Require Export Metalib.CoqEqDec.
+Require Export Metalib.CoqListFacts.
+Require Export Metalib.LibTactics.
+Require Export Metalib.MetatheoryAtom.
 
 
 (* ********************************************************************** *)
@@ -292,5 +292,5 @@ Ltac apply_fresh_base H gather_vars atom_name :=
 
 (* SCW added this one for list support *)
 Set Implicit Arguments.
-Definition union_map (A:Set) (f:A -> vars) (l:list A) := 
+Definition union_map (A:Set) (f:A -> vars) (l:list A) :=
  (List.fold_right (fun t acc => f t \u acc) {}) l.
diff --git a/MetatheoryAlt.v b/MetatheoryAlt.v
index 5b8b515..6e9cdda 100644
--- a/MetatheoryAlt.v
+++ b/MetatheoryAlt.v
@@ -10,13 +10,13 @@ Require Export Coq.Arith.Arith.
 Require Export Coq.FSets.FSets.
 Require Export Coq.Lists.List.
 
-Require Export CoqEqDec.
-Require Export CoqListFacts.
-Require Export LibTactics.
-Require Export MetatheoryAtom.
+Require Export Metalib.CoqEqDec.
+Require Export Metalib.CoqListFacts.
+Require Export Metalib.LibTactics.
+Require Export Metalib.MetatheoryAtom.
 (* Require Export MetatheoryEnv. *)
 
-Require Export AssumeList.
+Require Export Metalib.AssumeList.
 
 (* ********************************************************************** *)
 (** * Decidable equality *)
@@ -94,7 +94,7 @@ Open Scope set_hs_scope.
     standard recursive notation for lists, e.g., the one found in the
     Program library of Coq's standard library. *)
 
-(* Notation "[ x ]" := (EnvImpl.one x) : env_scope. 
+(* Notation "[ x ]" := (EnvImpl.one x) : env_scope.
 
 Open Scope env_scope.
 *)
diff --git a/MetatheoryAtom.v b/MetatheoryAtom.v
index 3664f90..6c48242 100644
--- a/MetatheoryAtom.v
+++ b/MetatheoryAtom.v
@@ -12,11 +12,11 @@ Require Import Coq.Classes.EquivDec.
 Require Import Coq.Lists.List.
 Require Import Coq.Structures.DecidableTypeEx.
 
-Require Import CoqFSetDecide.
-Require Import CoqListFacts.
-Require Import FSetExtra.
-Require Import FSetWeakNotin.
-Require Import LibTactics.
+Require Import Metalib.CoqFSetDecide.
+Require Import Metalib.CoqListFacts.
+Require Import Metalib.FSetExtra.
+Require Import Metalib.FSetWeakNotin.
+Require Import Metalib.LibTactics.
 
 Require Import Omega.
 
diff --git a/STLC.v b/STLC.v
index 8658251..36f3991 100644
--- a/STLC.v
+++ b/STLC.v
@@ -56,7 +56,7 @@
     directory to compile the Metatheory library.
 *)
 
-Require Import Metatheory.
+Require Import Metalib.Metatheory.
 
 
 (*************************************************************************)
@@ -1215,7 +1215,7 @@ Proof.
   induction H; intros G Eq Uniq; subst.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.
 
-     
+
 
 (** *** Example
 
@@ -1339,7 +1339,7 @@ Lemma typing_c_subst : forall (E F : env) e u S T (z : atom),
 Proof.
 (* FILL IN HERE (and delete "Admitted") *) Admitted.
 
-        
+
 (** *** Exercise
 
     Complete the proof of the substitution lemma stated in the form we
diff --git a/STLCsol.v b/STLCsol.v
index 1e15401..f89fad6 100644
--- a/STLCsol.v
+++ b/STLCsol.v
@@ -56,7 +56,7 @@
     directory to compile the Metatheory library.
 *)
 
-Require Import Metatheory.
+Require Import Metalib.Metatheory.
 
 
 (*************************************************************************)
@@ -1330,7 +1330,7 @@ Proof.
       apply binds_weaken. apply H0.
   Case "typing_abs_c".
 
-     
+
     pick fresh x and apply typing_abs_c.
     rewrite_env (((x ~ T1) ++ G) ++ F ++ E).
     apply H0.
@@ -1494,7 +1494,7 @@ Proof.
     subst.
     simpl.
 
-        
+
     pick fresh y and apply typing_abs_c.
     rewrite subst_open_var_c.
     rewrite_env (((y ~ T1) ++ F) ++ E).