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\
130 VOFILES=$(VFILES:.v=.vo)
131 VIFILES=$(VFILES:.v=.vi)
132 GFILES=$(VFILES:.v=.g)
133 HTMLFILES=$(VFILES:.v=.html)
134 GHTMLFILES=$(VFILES:.v=.g.html)
136 all: base_tactics.vo\
153 subst0_confluence.vo\
159 subst1_confluence.vo\
208 gallinahtml: $(GHTMLFILES)
211 $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
213 all-gal.ps: $(GFILES)
214 $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`
216 xml:: .xml_time_stamp
217 .xml_time_stamp: base_tactics.vo\
234 subst0_confluence.vo\
240 subst1_confluence.vo\
282 $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
283 touch .xml_time_stamp
291 .PHONY: all opt byte archclean clean install depend xml
293 .SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
296 $(COQC) $(COQDEBUG) $(COQFLAGS) $*
299 $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
308 $(COQWEB) -html $< -o $@
314 $(COQWEB) -html $< -o $@
320 $(MAKE) all "OPT=-opt"
326 $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
327 $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
332 mkdir -p `$(COQC) -where`/user-contrib
333 cp -f *.vo `$(COQC) -where`/user-contrib
336 mv -f Makefile Makefile.bak
337 $(COQBIN)coq_makefile -f Make -o Makefile
340 rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
341 rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
348 # This Makefile has been automagically generated by coq_makefile
349 # Edit at your own risks !