aboutsummaryrefslogtreecommitdiff
path: root/doc/Makefile
diff options
context:
space:
mode:
authorbarras2002-12-17 15:21:18 +0000
committerbarras2002-12-17 15:21:18 +0000
commite7c64da4552460c5e888e23a03ac1bb94982915d (patch)
tree876a2e7f4ccfce7301e7e94f48a95eeb4b0ae8f7 /doc/Makefile
parentdca7ee4971140f1c02f9e9d742376f61b0663499 (diff)
exemple complet de parser
changement de syntaxe des scope: expr % id ex: (10 + 5 * 4)%N ou 4%N git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3451 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile35
1 files changed, 33 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 47a102fd91..9d8ea2ee3a 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,7 +1,38 @@
# Makefile for doc/
-all: newsyntax.dvi minicoq.dvi
+all:: newparse
+#newsyntax.dvi minicoq.dvi
+
+
+OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo
+
+newparse: $(OBJS) syntax.mli lex.ml syntax.ml
+ ocamlc -o newparse $(OBJS)
+
+.ml.cmo:
+ ocamlc -c $<
+
+.mli.cmi:
+ ocamlc -c $<
+
+.mll.ml:
+ ocamllex $<
+
+.mly.ml:
+ ocamlyacc -v $<
+
+.mly.mli:
+ ocamlyacc -v $<
+
+clean::
+ rm -f *.cm* *.output syntax.ml syntax.mli lex.ml newparse
+
+parse.cmo: ast.cmo
+syntax.cmi: parse.cmo
+syntax.cmo: lex.cmo parse.cmo syntax.cmi
+lex.cmo: syntax.cmi
+ast.cmo: ast.ml
newsyntax.dvi: newsyntax.tex
latex $<
@@ -26,7 +57,7 @@ depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
clean::
rm -f *~ *.log *.aux
-.SUFFIXES: .tex .dvi .ps
+.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly
.tex.dvi:
latex $< && latex $<