1 ##############################################################################
2 ## The Calculus of Inductive Constructions ##
7 ## Rocquencourt Lyon ##
12 ##############################################################################
16 # This Makefile has been automagically generated by coq_makefile
17 # Edit at your own risks !
22 # This Makefile was generated by the command line :
23 # coq_makefile -f Make -o Makefile
26 ##########################
28 # Variables definitions. #
30 ##########################
32 CAMLP4LIB=`camlp4 -where`
33 COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
34 -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
35 -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
36 -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
37 ZFLAGS=$(OCAMLLIBS) $(COQSRC)
39 COQFLAGS=-q $(OPT) $(COQLIBS)
47 COQDEP=$(COQBIN)coqdep -c
50 #########################
52 # Libraries definition. #
54 #########################
59 ###################################
61 # Definition of the "all" target. #
63 ###################################
65 VFILES=base_tactics.v\
133 VOFILES=$(VFILES:.v=.vo)
134 VIFILES=$(VFILES:.v=.vi)
135 GFILES=$(VFILES:.v=.g)
136 HTMLFILES=$(VFILES:.v=.html)
137 GHTMLFILES=$(VFILES:.v=.g.html)
139 all: base_tactics.vo\
158 subst0_confluence.vo\
164 subst1_confluence.vo\
214 gallinahtml: $(GHTMLFILES)
217 $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
219 all-gal.ps: $(GFILES)
220 $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`
222 xml:: .xml_time_stamp
223 .xml_time_stamp: base_tactics.vo\
242 subst0_confluence.vo\
248 subst1_confluence.vo\
291 $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
292 touch .xml_time_stamp
300 .PHONY: all opt byte archclean clean install depend xml
302 .SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
305 $(COQC) $(COQDEBUG) $(COQFLAGS) $*
308 $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
317 $(COQWEB) -html $< -o $@
323 $(COQWEB) -html $< -o $@
329 $(MAKE) all "OPT=-opt"
335 $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
336 $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
341 mkdir -p `$(COQC) -where`/user-contrib
342 cp -f *.vo `$(COQC) -where`/user-contrib
345 mv -f Makefile Makefile.bak
346 $(COQBIN)coq_makefile -f Make -o Makefile
349 rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
350 rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
357 # This Makefile has been automagically generated by coq_makefile
358 # Edit at your own risks !