From a47b49b11d17add5ca1ea5e650d2f344219b4f7e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 5 Feb 2016 15:24:42 -0500
Subject: Update build process to use COQPATH & _CoqProject

Removed all of the files not built by default; they can be resurrected from git
history.  _CoqProject is the standard way to list the files in a project and to
give information to coq_makefile.  COQPATH is the standard way to make use of
not-yet-installed libraries that are not part of your project (i.e., you don't
want to remove them when you `make clean`, etc.).
---
 coqprime/Coqprime/Makefile.bak | 203 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 203 insertions(+)
 create mode 100644 coqprime/Coqprime/Makefile.bak

(limited to 'coqprime/Coqprime/Makefile.bak')

diff --git a/coqprime/Coqprime/Makefile.bak b/coqprime/Coqprime/Makefile.bak
new file mode 100644
index 000000000..fe49dbf29
--- /dev/null
+++ b/coqprime/Coqprime/Makefile.bak
@@ -0,0 +1,203 @@
+##############################################################################
+##                 The Calculus of Inductive Constructions                  ##
+##                                                                          ##
+##                                Projet Coq                                ##
+##                                                                          ##
+##                     INRIA                        ENS-CNRS                ##
+##              Rocquencourt                        Lyon                    ##
+##                                                                          ##
+##                                  Coq V7                                  ##
+##                                                                          ##
+##                                                                          ##
+##############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -f Make -o Makefile 
+#
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+CAMLP4LIB=`camlp4 -where`
+COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
+  -I $(COQTOP)/library -I $(COQTOP)/parsing \
+  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \
+  -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
+  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \
+  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \
+  -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \
+  -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \
+  -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \
+  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \
+  -I $(CAMLP4LIB)
+ZFLAGS=$(OCAMLLIBS) $(COQSRC)
+OPT=
+COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQC=$(COQBIN)coqc
+GALLINA=gallina
+COQDOC=coqdoc
+CAMLC=ocamlc -c
+CAMLOPTC=ocamlopt -c
+CAMLLINK=ocamlc
+CAMLOPTLINK=ocamlopt
+COQDEP=$(COQBIN)coqdep -c
+GRAMMARS=grammar.cma
+CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo
+PP=-pp "camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl"
+
+#########################
+#                       #
+# Libraries definition. #
+#                       #
+#########################
+
+OCAMLLIBS=-I .\
+  -I ../Tactic\
+  -I ../N\
+  -I ../Z\
+  -I ../List
+COQLIBS=-I .\
+  -I ../Tactic\
+  -I ../N\
+  -I ../Z\
+  -I ../List
+
+###################################
+#                                 #
+# Definition of the "all" target. #
+#                                 #
+###################################
+
+VFILES=Cyclic.v\
+  EGroup.v\
+  Euler.v\
+  FGroup.v\
+  IGroup.v\
+  Lagrange.v\
+  LucasLehmer.v\
+  Pepin.v\
+  PGroup.v\
+  PocklingtonCertificat.v\
+  PocklingtonRefl.v\
+  Pocklington.v\
+  Proth.v\
+  Root.v\
+  Zp.v
+VOFILES=$(VFILES:.v=.vo)
+VIFILES=$(VFILES:.v=.vi)
+GFILES=$(VFILES:.v=.g)
+HTMLFILES=$(VFILES:.v=.html)
+GHTMLFILES=$(VFILES:.v=.g.html)
+
+all: Cyclic.vo\
+  EGroup.vo\
+  Euler.vo\
+  FGroup.vo\
+  IGroup.vo\
+  Lagrange.vo\
+  LucasLehmer.vo\
+  Pepin.vo\
+  PGroup.vo\
+  PocklingtonCertificat.vo\
+  PocklingtonRefl.vo\
+  Pocklington.vo\
+  Proth.vo\
+  Root.vo\
+  Zp.vo
+
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(HTMLFILES)
+
+gallinahtml: $(GHTMLFILES)
+
+all.ps: $(VFILES)
+	$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.ps: $(VFILES)
+	$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+.PHONY: all opt byte archclean clean install depend html
+
+.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
+
+.v.vo:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+.v.vi:
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+.v.g:
+	$(GALLINA) $<
+
+.v.tex:
+	$(COQDOC) -latex $< -o $@
+
+.v.html:
+	$(COQDOC) -html $< -o $@
+
+.v.g.tex:
+	$(COQDOC) -latex -g $< -o $@
+
+.v.g.html:
+	$(COQDOC) -html -g $< -o $@
+
+byte:
+	$(MAKE) all "OPT="
+
+opt:
+	$(MAKE) all "OPT=-opt"
+
+include .depend
+
+.depend depend:
+	rm -f .depend
+	$(COQDEP) -i $(COQLIBS) $(VFILES) *.ml *.mli >.depend
+	$(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend
+
+install:
+	mkdir -p `$(COQC) -where`/user-contrib
+	cp -f $(VOFILES) `$(COQC) -where`/user-contrib
+
+Makefile: Make
+	mv -f Makefile Makefile.bak
+	$(COQBIN)coq_makefile -f Make -o Makefile
+
+
+clean:
+	rm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~
+	rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
+
+archclean:
+	rm -f *.cmx *.o
+
+html:
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
-- 
cgit v1.2.3