update makefiles for new directory structure

Fsub/Fsub_LetSum_Infrastructure.v

@@ -19,7 +19,7 @@
       - #<a href="##auto">Automation</a>#
       - #<a href="##body">Properties of body_e</a># *)
 
-Require Export Metalib.Fsub_LetSum_Definitions.
+Require Export Fsub.Fsub_LetSum_Definitions.
 
 
 (* ********************************************************************** *)

Fsub/Fsub_LetSum_Lemmas.v

@@ -21,7 +21,7 @@
       - #<a href="##regularity">Regularity lemmas</a>#
       - #<a href="##auto">Automation</a># *)
 
-Require Export Metalib.Fsub_LetSum_Infrastructure.
+Require Export Fsub.Fsub_LetSum_Infrastructure.
 
 
 (* ********************************************************************** *)

Fsub/Fsub_LetSum_Soundness.v

@@ -12,7 +12,7 @@
       - #<a href="##preservation">Preservation</a>#
       - #<a href="##progress">Progress</a># *)
 
-Require Export Metalib.Fsub_LetSum_Lemmas.
+Require Export Fsub.Fsub_LetSum_Lemmas.
 
 
 (* ********************************************************************** *)

Fsub/Makefile

@@ -0,0 +1,65 @@
+############################################################################
+#
+#  Primary targets:
+#    all           - the default target; synonym for 'coq'
+#    coq           - builds all .vo files
+#    doc           - synonym for 'documentation'
+#    install       - copy to coq library location
+#    clean         - removes generated files
+#
+#  Other targets (intended to be used by the developers of this library):
+#    gens          - builds generated .v files on demand
+#    dist          - builds a zip file for distribution
+#
+############################################################################
+
+## Paths to executables. Do not include options here.
+## Modify these to suit your Coq installation, if necessary.
+
+## If you get warnings such as:
+## *** Warning: in file AssocList.v, library CoqFSetDecide is required and has not been found in the loadpath!
+## you can use a shell variable to set the load path. (Somehow the -I below is being ignored.)
+## export COQPATH=.
+
+COQC = coqc
+COQDEP = coqdep
+COQDOC = coqdoc
+
+
+## Library name used for the imports in Coq
+
+LIBNAME=Fsub
+
+## Name of the submakefile generated by coq_makefile
+
+COQMKFILENAME=CoqSrc.mk
+
+
+############################################################################
+
+.PHONY: all clean coq dist doc gens
+.SUFFIXES: .v .vo .v.d .v.glob
+
+all: coq
+
+%.mk : Makefile _%
+	coq_makefile -f _$* -o $*.mk
+
+$(COQMKFILENAME): Makefile
+	{ echo "-R . $(LIBNAME) " ; ls *.v ; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME)
+
+coq: $(COQMKFILENAME)
+	@$(MAKE) -f $(COQMKFILENAME)
+
+doc:
+	@$(MAKE) -f $(COQMKFILENAME) html
+
+install:
+	@$(MAKE) -f $(COQMKFILENAME) install
+
+clean:
+	@$(MAKE) -f $(COQMKFILENAME) clean
+	rm -if $(COQMKFILENAME)
+
+
+############################################################################

Metalib/Makefile

@@ -0,0 +1,87 @@
+############################################################################
+#
+#  Primary targets:
+#    all           - the default target; synonym for 'coq'
+#    coq           - builds all .vo files
+#    doc           - synonym for 'documentation'
+#    install       - copy to coq library location
+#    clean         - removes generated files
+#
+#  Other targets (intended to be used by the developers of this library):
+#    gens          - builds generated .v files on demand
+#    dist          - builds a zip file for distribution
+#
+############################################################################
+
+## Paths to executables. Do not include options here.
+## Modify these to suit your Coq installation, if necessary.
+
+## If you get warnings such as:
+## *** Warning: in file AssocList.v, library CoqFSetDecide is required and has not been found in the loadpath!
+## you can use a shell variable to set the load path. (Somehow the -I below is being ignored.)
+## export COQPATH=.
+
+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
+
+
+############################################################################
+
+.PHONY: all clean coq dist doc gens
+.SUFFIXES: .v .vo .v.d .v.glob
+
+all: coq
+
+%.mk : Makefile _%
+	coq_makefile -f _$* -o $*.mk
+
+$(COQMKFILENAME): Makefile
+	{ echo "-R . $(LIBNAME) " ; ls *.v ; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME)
+
+coq: $(COQMKFILENAME)
+	@$(MAKE) -f $(COQMKFILENAME)
+
+doc:
+	@$(MAKE) -f $(COQMKFILENAME) html
+
+install:
+	@$(MAKE) -f $(COQMKFILENAME) install
+
+clean:
+	@$(MAKE) -f $(COQMKFILENAME) clean
+	rm -if $(COQMKFILENAME)
+
+
+############################################################################
+
+DATE = $(shell date +%Y%m%d)
+DIR  = metalib-$(DATE)
+
+COQSPLIT = ../../books/sf/tools/coqsplit
+STLC = ../../books/coqbook/stlc/STLC.v
+
+gens:
+	make -C ../../books/sf tools/coqsplit
+	$(COQSPLIT) < $(STLC) > STLC.v
+	$(COQSPLIT) -solutions < $(STLC) > STLCsol.v
+
+dist:
+	svn export . $(DIR)
+	(cd $(DIR); $(MAKE) documentation)
+	rm -f $(DIR)/*.vo $(DIR)/*.glob
+	rm -f $(DIR)/TODO.txt
+	echo Release $(DATE) / svn revision `svnversion .` >> $(DIR)/VERSION
+	zip -r $(DIR).zip $(DIR)
+	@echo
+	@echo Done.
+	@echo See $(DIR) and $(DIR).zip.

Tutorial/Makefile

@@ -0,0 +1,65 @@
+############################################################################
+#
+#  Primary targets:
+#    all           - the default target; synonym for 'coq'
+#    coq           - builds all .vo files
+#    doc           - synonym for 'documentation'
+#    install       - copy to coq library location
+#    clean         - removes generated files
+#
+#  Other targets (intended to be used by the developers of this library):
+#    gens          - builds generated .v files on demand
+#    dist          - builds a zip file for distribution
+#
+############################################################################
+
+## Paths to executables. Do not include options here.
+## Modify these to suit your Coq installation, if necessary.
+
+## If you get warnings such as:
+## *** Warning: in file AssocList.v, library CoqFSetDecide is required and has not been found in the loadpath!
+## you can use a shell variable to set the load path. (Somehow the -I below is being ignored.)
+## export COQPATH=.
+
+COQC = coqc
+COQDEP = coqdep
+COQDOC = coqdoc
+
+
+## Library name used for the imports in Coq
+
+LIBNAME=Stlc
+
+## Name of the submakefile generated by coq_makefile
+
+COQMKFILENAME=CoqSrc.mk
+
+
+############################################################################
+
+.PHONY: all clean coq dist doc gens
+.SUFFIXES: .v .vo .v.d .v.glob
+
+all: coq
+
+%.mk : Makefile _%
+	coq_makefile -f _$* -o $*.mk
+
+$(COQMKFILENAME): Makefile
+	{ echo "-R . $(LIBNAME) " ; ls *.v ; } > _CoqProject && coq_makefile -f _CoqProject -o $(COQMKFILENAME)
+
+coq: $(COQMKFILENAME)
+	@$(MAKE) -f $(COQMKFILENAME)
+
+doc:
+	@$(MAKE) -f $(COQMKFILENAME) html
+
+install:
+	@$(MAKE) -f $(COQMKFILENAME) install
+
+clean:
+	@$(MAKE) -f $(COQMKFILENAME) clean
+	rm -if $(COQMKFILENAME)
+
+
+############################################################################

Tutorial/STLC.v

@@ -331,7 +331,7 @@ Proof.
   Case "bvar".
     assumption.
   Case "fvar".
-    destruct (a == y).
+  destruct (a == y).
       assumption.
       simpl. assumption.
   Case "abs".
@@ -1901,4 +1901,3 @@ Proof.
   Case "typing_abs".
         apply typing_abs with (x:=x). auto.
 Admitted.
-

Tutorial/STLCsol.v

@@ -2151,4 +2151,3 @@ Proof.
   Case "typing_abs".
         apply typing_abs with (x:=x). auto.
 Admitted.
-

doc/changes.html

@@ -69,6 +69,20 @@ <h1>Change log for the metatheory library</h1>
   releases.  The releases are listed in reverse chronological order.
 </p>
 
+<h2>coq8.6</h2>
+
+<ul><li>Compatibility changes with Coq 8.6</li>
+    <li>Moved examples to separate directories </li>
+</ul>
+
+<h2>coq8.5</h2>
+
+<ul><li>Compatibility changes with Coq 8.5</li></ul>
+
+<h2>coq8.4</h2>
+
+<ul><li>Moved repository to github</li></ul>
+
 <h2>20090714</h2>
 
 <ul>