summaryrefslogtreecommitdiff
path: root/dev/ocamlweb-doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ocamlweb-doc')
-rw-r--r--dev/ocamlweb-doc/Makefile90
-rw-r--r--dev/ocamlweb-doc/ast.ml47
-rw-r--r--dev/ocamlweb-doc/interp.dep.ps545
-rw-r--r--dev/ocamlweb-doc/intro.tex25
-rw-r--r--dev/ocamlweb-doc/kernel.dep.ps1431
-rw-r--r--dev/ocamlweb-doc/lex.mll81
-rw-r--r--dev/ocamlweb-doc/library.dep.ps773
-rw-r--r--dev/ocamlweb-doc/macros.tex7
-rw-r--r--dev/ocamlweb-doc/parse.ml183
-rw-r--r--dev/ocamlweb-doc/parsing.dep.ps1115
-rw-r--r--dev/ocamlweb-doc/preamble.tex8
-rw-r--r--dev/ocamlweb-doc/pretyping.dep.ps1259
-rw-r--r--dev/ocamlweb-doc/proofs.dep.ps649
-rw-r--r--dev/ocamlweb-doc/syntax.mly224
-rw-r--r--dev/ocamlweb-doc/tactics.dep.ps991
-rw-r--r--dev/ocamlweb-doc/toplevel.dep.ps971
16 files changed, 0 insertions, 8399 deletions
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
deleted file mode 100644
index 3189d7c5..00000000
--- a/dev/ocamlweb-doc/Makefile
+++ /dev/null
@@ -1,90 +0,0 @@
-include ../../config/Makefile
-
-LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
- -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \
- -I ../../proofs -I ../../tactics -I ../../pretyping \
- -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \
- -I ../../plugins/omega -I ../../plugins/romega \
- -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \
- -I ../../plugins/xml -I ../../plugins/extraction \
- -I ../../plugins/fourier \
- -I ../../plugins/cc \
- -I ../../plugins/funind -I ../../plugins/firstorder \
- -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \
- -I ../../plugins/recdef
-
-MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-
-
-all:: newparse coq.ps minicop.ps
-#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)
-
-%.cmo: %.ml
- ocamlc -c $<
-
-%.cmi: %.mli
- ocamlc -c $<
-
-%.ml: %.mll
- ocamllex $<
-
-%.ml: %.mly
- ocamlyacc -v $<
-
-%.mli: %.mly
- 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 $<
- latex $<
-
-coq.dvi: coq.tex
- latex coq
- latex coq
-
-coq.tex::
- ocamlweb -p "\usepackage{epsfig}" \
- macros.tex intro.tex \
- ../../lib/{doc.tex,*.mli} ../../kernel/{doc.tex,*.mli} ../../library/{doc.tex,*.mli} \
- ../../pretyping/{doc.tex,*.mli} ../../interp/{doc.tex,*.mli} \
- ../../parsing/{doc.tex,*.mli} ../../proofs/{doc.tex,*.mli} \
- ../../tactics/{doc.tex,*.mli} ../../toplevel/{doc.tex,*.mli} \
- -o coq.tex
-
-
-depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
- proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps
-
-%.dot: ../../%
- ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../../$*/*.ml ../../$*/*.mli -o $@
-
-%.dep.ps: %.dot
- dot -Tps $< -o $@
-
-clean::
- rm -f *~ *.log *.aux
-
-.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly
-
-%.dvi: %.tex
- latex $< && latex $<
-
-%.ps: %.dvi
- dvips $< -o $@
-
-
diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml
deleted file mode 100644
index 4eb135d8..00000000
--- a/dev/ocamlweb-doc/ast.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-
-type constr_ast =
- Pair of constr_ast * constr_ast
-| Prod of binder list * constr_ast
-| Lambda of binder list * constr_ast
-| Let of string * constr_ast * constr_ast
-| LetCase of binder list * constr_ast * constr_ast
-| IfCase of constr_ast * constr_ast * constr_ast
-| Eval of red_fun * constr_ast
-| Infix of string * constr_ast * constr_ast
-| Prefix of string * constr_ast
-| Postfix of string * constr_ast
-| Appl of constr_ast * constr_arg list
-| ApplExpl of string list * constr_ast list
-| Scope of string * constr_ast
-| Qualid of string list
-| Prop | Set | Type
-| Int of string
-| Hole
-| Meta of string
-| Fixp of fix_kind *
- (string * binder list * constr_ast * string option * constr_ast) list *
- string
-| Match of case_item list * constr_ast option *
- (pattern list * constr_ast) list
-
-and red_fun = Simpl
-
-and binder = string * constr_ast
-
-and constr_arg = string option * constr_ast
-
-and fix_kind = Fix | CoFix
-
-and case_item = constr_ast * (string option * constr_ast option)
-
-and pattern =
- PatAs of pattern * string
-| PatType of pattern * constr_ast
-| PatConstr of string * pattern list
-| PatVar of string
-
-let mk_cast c t =
- if t=Hole then c else Infix(":",c,t)
-
-let mk_lambda bl t =
- if bl=[] then t else Lambda(bl,t)
diff --git a/dev/ocamlweb-doc/interp.dep.ps b/dev/ocamlweb-doc/interp.dep.ps
deleted file mode 100644
index fda7a33c..00000000
--- a/dev/ocamlweb-doc/interp.dep.ps
+++ /dev/null
@@ -1,545 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
-%%For: (notin) Jean-Marc Notin,,,
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: (atend)
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-EncodingVector 45 /hyphen put
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-setupLatin1
-%%Page: 1 1
-%%PageBoundingBox: 36 36 576 753
-%%PageOrientation: Landscape
-gsave
-36 36 576 753 boxprim clip newpath
-0 0 1 beginpage
-0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 544 lineto
-724 544 lineto
-724 -4 lineto
-closepath fill
-0.985401 setlinewidth
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 544 lineto
-724 544 lineto
-724 -4 lineto
-closepath stroke
-% Constrextern
-gsave
-0.502 1.000 0.820 nodecolor
-172 417 49.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-172 417 49.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-172 412 moveto 72 -0.5 (Constrextern) alignedtext
-grestore
-% Reserve
-gsave
-0.502 1.000 0.820 nodecolor
-264 319 35.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-264 319 35.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-264 314 moveto 44 -0.5 (Reserve) alignedtext
-grestore
-% Constrextern->Reserve
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 188 400 moveto
-203 384 225 361 242 343 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 245.049 344.831 moveto
-249 335 lineto
-239.781 340.221 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 245.049 344.831 moveto
-249 335 lineto
-239.781 340.221 lineto
-closepath stroke
-grestore
-% Notation
-gsave
-0.502 1.000 0.820 nodecolor
-268 122 37.1753 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-268 122 37.1753 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-268 117 moveto 49 -0.5 (Notation) alignedtext
-grestore
-% Constrextern->Notation
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 178 399 moveto
-194 349 240 209 259 150 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 262.479 150.584 moveto
-262 140 lineto
-255.774 148.573 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 262.479 150.584 moveto
-262 140 lineto
-255.774 148.573 lineto
-closepath stroke
-grestore
-% Topconstr
-gsave
-0.502 1.000 0.820 nodecolor
-82 24 41.1755 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-82 24 41.1755 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-82 19 moveto 57 -0.5 (Topconstr) alignedtext
-grestore
-% Notation->Topconstr
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 243 109 moveto
-211 91 154 62 117 43 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 118.441 39.7969 moveto
-108 38 lineto
-115.042 45.916 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 118.441 39.7969 moveto
-108 38 lineto
-115.042 45.916 lineto
-closepath stroke
-grestore
-% Ppextend
-gsave
-0.502 1.000 0.820 nodecolor
-278 24 39.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-278 24 39.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-278 19 moveto 52 -0.5 (Ppextend) alignedtext
-grestore
-% Notation->Ppextend
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 270 104 moveto
-272 89 273 68 275 52 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 278.488 52.2987 moveto
-276 42 lineto
-271.522 51.6021 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 278.488 52.2987 moveto
-276 42 lineto
-271.522 51.6021 lineto
-closepath stroke
-grestore
-% Constrintern
-gsave
-0.502 1.000 0.820 nodecolor
-472 417 48.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-472 417 48.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-472 412 moveto 70 -0.5 (Constrintern) alignedtext
-grestore
-% Constrintern->Reserve
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 442 403 moveto
-404 385 340 355 299 335 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 300.56 331.863 moveto
-290 331 lineto
-297.717 338.26 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 300.56 331.863 moveto
-290 331 lineto
-297.717 338.26 lineto
-closepath stroke
-grestore
-% Implicit_quantifiers
-gsave
-0.502 1.000 0.820 nodecolor
-508 319 69.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-508 319 69.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-508 314 moveto 112 -0.5 (Implicit_quantifiers) alignedtext
-grestore
-% Constrintern->Implicit_quantifiers
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 479 399 moveto
-484 385 492 364 498 347 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 501.479 347.584 moveto
-501 337 lineto
-494.774 345.573 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 501.479 347.584 moveto
-501 337 lineto
-494.774 345.573 lineto
-closepath stroke
-grestore
-% Syntax_def
-gsave
-0.502 1.000 0.820 nodecolor
-396 220 45.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-396 220 45.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-396 215 moveto 64 -0.5 (Syntax_def) alignedtext
-grestore
-% Implicit_quantifiers->Syntax_def
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 488 302 moveto
-469 285 442 261 422 244 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 424.546 241.596 moveto
-415 237 lineto
-419.596 246.546 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 424.546 241.596 moveto
-415 237 lineto
-419.596 246.546 lineto
-closepath stroke
-grestore
-% Coqlib
-gsave
-0.502 1.000 0.820 nodecolor
-656 515 32.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-656 515 32.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-656 510 moveto 38 -0.5 (Coqlib) alignedtext
-grestore
-% Genarg
-gsave
-0.502 1.000 0.820 nodecolor
-82 122 33.175 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-82 122 33.175 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-82 117 moveto 41 -0.5 (Genarg) alignedtext
-grestore
-% Genarg->Topconstr
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 82 104 moveto
-82 89 82 69 82 52 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 85.5001 52 moveto
-82 42 lineto
-78.5001 52 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 85.5001 52 moveto
-82 42 lineto
-78.5001 52 lineto
-closepath stroke
-grestore
-% Syntax_def->Notation
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 375 204 moveto
-354 187 320 161 296 143 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 298.1 140.2 moveto
-288 137 lineto
-293.9 145.8 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 298.1 140.2 moveto
-288 137 lineto
-293.9 145.8 lineto
-closepath stroke
-grestore
-% Modintern
-gsave
-0.502 1.000 0.820 nodecolor
-472 515 42.1756 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-472 515 42.1756 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-472 510 moveto 59 -0.5 (Modintern) alignedtext
-grestore
-% Modintern->Constrintern
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 472 497 moveto
-472 482 472 462 472 445 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 475.5 445 moveto
-472 435 lineto
-468.5 445 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 475.5 445 moveto
-472 435 lineto
-468.5 445 lineto
-closepath stroke
-grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-%%BoundingBox: 36 36 576 753
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/intro.tex b/dev/ocamlweb-doc/intro.tex
deleted file mode 100644
index 4cec8673..00000000
--- a/dev/ocamlweb-doc/intro.tex
+++ /dev/null
@@ -1,25 +0,0 @@
-
-\ocwsection This is \Coq, a proof assistant for the \CCI.
-This document describes the implementation of \Coq.
-It has been automatically generated from the source of
-\Coq\ using \textsf{ocamlweb}, a literate programming tool for
-\textsf{Objective Caml}\footnote{\Coq, \textsf{Objective Caml} and
- \textsf{ocamlweb} are all freely available at
- \textsf{http://coq.inria.fr/}, \textsf{http://caml.inria.fr/} and
- \textsf{http://www.lri.fr/\~{}filliatr/ocamlweb}.}.
-The source files are organized in several directories, which are
-described here as separate chapters.
-
-\begin{center}
- \begin{tabular}{p{10cm}rr}
- Chapter & section & page \\[0.5em]
- \hline\\[0.2em]
- Utility libraries \dotfill & \refsec{lib} & \pageref{lib} \\[0.5em]
- Kernel \dotfill & \refsec{kernel} & \pageref{kernel} \\[0.5em]
- Library \dotfill & \refsec{library} & \pageref{library} \\[0.5em]
- Pretyping \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em]
- Proof engine \dotfill & \refsec{proofs} & \pageref{proofs} \\[0.5em]
- Tactics \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em]
- Toplevel \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em]
- \end{tabular}
-\end{center} \ No newline at end of file
diff --git a/dev/ocamlweb-doc/kernel.dep.ps b/dev/ocamlweb-doc/kernel.dep.ps
deleted file mode 100644
index b7b4137b..00000000
--- a/dev/ocamlweb-doc/kernel.dep.ps
+++ /dev/null
@@ -1,1431 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
-%%For: (notin) Jean-Marc Notin,,,
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: (atend)
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-EncodingVector 45 /hyphen put
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-setupLatin1
-%%Page: 1 1
-%%PageBoundingBox: 36 36 535 756
-%%PageOrientation: Landscape
-gsave
-36 36 535 756 boxprim clip newpath
-0 0 1 beginpage
-0.393658 0.393658 set_scale 90 rotate 95.45 -1355.45 translate
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 1264 lineto
-1825 1264 lineto
-1825 -4 lineto
-closepath fill
-0.393658 setlinewidth
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 1264 lineto
-1825 1264 lineto
-1825 -4 lineto
-closepath stroke
-% Cbytecodes
-gsave
-0.502 1.000 0.820 nodecolor
-1258 234 45.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1258 234 45.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1258 229 moveto 64 -0.5 (Cbytecodes) alignedtext
-grestore
-% Term
-gsave
-0.502 1.000 0.820 nodecolor
-1093 162 28.1746 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1093 162 28.1746 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1093 157 moveto 31 -0.5 (Term) alignedtext
-grestore
-% Cbytecodes->Term
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1227 221 moveto
-1198 208 1155 189 1125 176 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1126.56 172.863 moveto
-1116 172 lineto
-1123.72 179.26 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1126.56 172.863 moveto
-1116 172 lineto
-1123.72 179.26 lineto
-closepath stroke
-grestore
-% Esubst
-gsave
-0.502 1.000 0.820 nodecolor
-1093 90 31.1748 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1093 90 31.1748 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1093 85 moveto 37 -0.5 (Esubst) alignedtext
-grestore
-% Term->Esubst
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1093 144 moveto
-1093 136 1093 127 1093 118 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1096.5 118 moveto
-1093 108 lineto
-1089.5 118 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1096.5 118 moveto
-1093 108 lineto
-1089.5 118 lineto
-closepath stroke
-grestore
-% Univ
-gsave
-0.502 1.000 0.820 nodecolor
-580 90 27.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-580 90 27.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-580 85 moveto 28 -0.5 (Univ) alignedtext
-grestore
-% Term->Univ
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1065 158 moveto
-979 145 714 109 616 95 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 616.299 91.5125 moveto
-606 94 lineto
-615.602 98.4778 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 616.299 91.5125 moveto
-606 94 lineto
-615.602 98.4778 lineto
-closepath stroke
-grestore
-% Cbytegen
-gsave
-0.502 1.000 0.820 nodecolor
-1148 522 39.1754 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1148 522 39.1754 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1148 517 moveto 53 -0.5 (Cbytegen) alignedtext
-grestore
-% Pre_env
-gsave
-0.502 1.000 0.820 nodecolor
-1148 450 36.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1148 450 36.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1148 445 moveto 46 -0.5 (Pre_env) alignedtext
-grestore
-% Cbytegen->Pre_env
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1148 504 moveto
-1148 496 1148 487 1148 478 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 478 moveto
-1148 468 lineto
-1144.5 478 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 478 moveto
-1148 468 lineto
-1144.5 478 lineto
-closepath stroke
-grestore
-% Declarations
-gsave
-0.502 1.000 0.820 nodecolor
-1148 378 48.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1148 378 48.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1148 373 moveto 70 -0.5 (Declarations) alignedtext
-grestore
-% Pre_env->Declarations
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1148 432 moveto
-1148 424 1148 415 1148 406 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 406 moveto
-1148 396 lineto
-1144.5 406 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 406 moveto
-1148 396 lineto
-1144.5 406 lineto
-closepath stroke
-grestore
-% Cemitcodes
-gsave
-0.502 1.000 0.820 nodecolor
-663 306 45.1757 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-663 306 45.1757 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-663 301 moveto 65 -0.5 (Cemitcodes) alignedtext
-grestore
-% Cemitcodes->Cbytecodes
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 706 301 moveto
-813 287 1088 254 1205 240 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1205.4 243.478 moveto
-1215 239 lineto
-1204.7 236.512 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1205.4 243.478 moveto
-1215 239 lineto
-1204.7 236.512 lineto
-closepath stroke
-grestore
-% Copcodes
-gsave
-0.502 1.000 0.820 nodecolor
-786 234 40.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-786 234 40.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-786 229 moveto 54 -0.5 (Copcodes) alignedtext
-grestore
-% Cemitcodes->Copcodes
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 688 291 moveto
-707 281 732 266 752 253 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 753.958 255.916 moveto
-761 248 lineto
-750.559 249.797 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 753.958 255.916 moveto
-761 248 lineto
-750.559 249.797 lineto
-closepath stroke
-grestore
-% Mod_subst
-gsave
-0.502 1.000 0.820 nodecolor
-325 234 43.1756 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-325 234 43.1756 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-325 229 moveto 61 -0.5 (Mod_subst) alignedtext
-grestore
-% Cemitcodes->Mod_subst
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 623 298 moveto
-561 284 441 259 374 244 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 374.492 240.529 moveto
-364 242 lineto
-373.119 247.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 374.492 240.529 moveto
-364 242 lineto
-373.119 247.393 lineto
-closepath stroke
-grestore
-% Mod_subst->Term
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 367 230 moveto
-502 217 925 178 1055 166 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1055.4 169.478 moveto
-1065 165 lineto
-1054.7 162.512 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1055.4 169.478 moveto
-1065 165 lineto
-1054.7 162.512 lineto
-closepath stroke
-grestore
-% Closure
-gsave
-0.502 1.000 0.820 nodecolor
-713 666 34.1751 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-713 666 34.1751 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-713 661 moveto 43 -0.5 (Closure) alignedtext
-grestore
-% Environ
-gsave
-0.502 1.000 0.820 nodecolor
-1148 594 36.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1148 594 36.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1148 589 moveto 46 -0.5 (Environ) alignedtext
-grestore
-% Closure->Environ
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 746 661 moveto
-823 648 1016 616 1104 602 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1104.88 605.393 moveto
-1114 600 lineto
-1103.51 598.529 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1104.88 605.393 moveto
-1114 600 lineto
-1103.51 598.529 lineto
-closepath stroke
-grestore
-% Environ->Cbytegen
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1148 576 moveto
-1148 568 1148 559 1148 550 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 550 moveto
-1148 540 lineto
-1144.5 550 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 550 moveto
-1148 540 lineto
-1144.5 550 lineto
-closepath stroke
-grestore
-% Conv_oracle
-gsave
-0.502 1.000 0.820 nodecolor
-383 522 48.1758 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-383 522 48.1758 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-383 517 moveto 71 -0.5 (Conv_oracle) alignedtext
-grestore
-% Names
-gsave
-0.502 1.000 0.820 nodecolor
-288 18 32.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-288 18 32.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-288 13 moveto 38 -0.5 (Names) alignedtext
-grestore
-% Conv_oracle->Names
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 339 515 moveto
-238 497 0 449 0 378 curveto
-0 378 0 378 0 162 curveto
-0 53 166 26 246 20 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 246.398 23.4778 moveto
-256 19 lineto
-245.701 16.5125 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 246.398 23.4778 moveto
-256 19 lineto
-245.701 16.5125 lineto
-closepath stroke
-grestore
-% Cooking
-gsave
-0.502 1.000 0.820 nodecolor
-960 1026 37.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-960 1026 37.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-960 1021 moveto 48 -0.5 (Cooking) alignedtext
-grestore
-% Typeops
-gsave
-0.502 1.000 0.820 nodecolor
-960 954 37.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-960 954 37.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-960 949 moveto 48 -0.5 (Typeops) alignedtext
-grestore
-% Cooking->Typeops
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 960 1008 moveto
-960 1000 960 991 960 982 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 963.5 982 moveto
-960 972 lineto
-956.5 982 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 963.5 982 moveto
-960 972 lineto
-956.5 982 lineto
-closepath stroke
-grestore
-% Entries
-gsave
-0.502 1.000 0.820 nodecolor
-1391 882 33.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1391 882 33.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1391 877 moveto 40 -0.5 (Entries) alignedtext
-grestore
-% Typeops->Entries
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 995 948 moveto
-1074 935 1265 903 1349 889 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1349.88 892.393 moveto
-1359 887 lineto
-1348.51 885.529 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1349.88 892.393 moveto
-1359 887 lineto
-1348.51 885.529 lineto
-closepath stroke
-grestore
-% Inductive
-gsave
-0.502 1.000 0.820 nodecolor
-837 882 39.1754 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-837 882 39.1754 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-837 877 moveto 53 -0.5 (Inductive) alignedtext
-grestore
-% Typeops->Inductive
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 936 940 moveto
-918 929 891 914 871 901 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 872.441 897.797 moveto
-862 896 lineto
-869.042 903.916 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 872.441 897.797 moveto
-862 896 lineto
-869.042 903.916 lineto
-closepath stroke
-grestore
-% Csymtable
-gsave
-0.502 1.000 0.820 nodecolor
-1148 666 42.1756 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1148 666 42.1756 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1148 661 moveto 59 -0.5 (Csymtable) alignedtext
-grestore
-% Csymtable->Environ
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1148 648 moveto
-1148 640 1148 631 1148 622 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 622 moveto
-1148 612 lineto
-1144.5 622 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 622 moveto
-1148 612 lineto
-1144.5 622 lineto
-closepath stroke
-grestore
-% Vm
-gsave
-0.502 1.000 0.820 nodecolor
-731 594 27 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-731 594 27 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-731 589 moveto 21 -0.5 (Vm) alignedtext
-grestore
-% Csymtable->Vm
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1109 659 moveto
-1029 645 845 614 767 600 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 767.492 596.529 moveto
-757 598 lineto
-766.119 603.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 767.492 596.529 moveto
-757 598 lineto
-766.119 603.393 lineto
-closepath stroke
-grestore
-% Vm->Cemitcodes
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 727 576 moveto
-716 527 684 392 669 334 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 672.393 333.119 moveto
-667 324 lineto
-665.529 334.492 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 672.393 333.119 moveto
-667 324 lineto
-665.529 334.492 lineto
-closepath stroke
-grestore
-% Vm->Conv_oracle
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 705 589 moveto
-648 577 510 549 435 533 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 435.492 529.529 moveto
-425 531 lineto
-434.119 536.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 435.492 529.529 moveto
-425 531 lineto
-434.119 536.393 lineto
-closepath stroke
-grestore
-% Declarations->Cemitcodes
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1103 371 moveto
-1013 358 811 328 715 314 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 715.492 310.529 moveto
-705 312 lineto
-714.119 317.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 715.492 310.529 moveto
-705 312 lineto
-714.119 317.393 lineto
-closepath stroke
-grestore
-% Sign
-gsave
-0.502 1.000 0.820 nodecolor
-1697 306 27 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1697 306 27 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1697 301 moveto 26 -0.5 (Sign) alignedtext
-grestore
-% Declarations->Sign
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1193 372 moveto
-1300 359 1563 324 1660 311 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1660.4 314.478 moveto
-1670 310 lineto
-1659.7 307.512 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1660.4 314.478 moveto
-1670 310 lineto
-1659.7 307.512 lineto
-closepath stroke
-grestore
-% Retroknowledge
-gsave
-0.502 1.000 0.820 nodecolor
-1221 306 59.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1221 306 59.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1221 301 moveto 92 -0.5 (Retroknowledge) alignedtext
-grestore
-% Declarations->Retroknowledge
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1165 361 moveto
-1175 352 1186 341 1197 330 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1199.4 332.546 moveto
-1204 323 lineto
-1194.45 327.596 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1199.4 332.546 moveto
-1204 323 lineto
-1194.45 327.596 lineto
-closepath stroke
-grestore
-% Sign->Term
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1671 300 moveto
-1576 277 1241 197 1130 170 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1130.49 166.529 moveto
-1120 168 lineto
-1129.12 173.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1130.49 166.529 moveto
-1120 168 lineto
-1129.12 173.393 lineto
-closepath stroke
-grestore
-% Retroknowledge->Cbytecodes
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1230 288 moveto
-1234 280 1239 270 1244 261 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1247.2 262.441 moveto
-1249 252 lineto
-1241.08 259.042 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1247.2 262.441 moveto
-1249 252 lineto
-1241.08 259.042 lineto
-closepath stroke
-grestore
-% Entries->Sign
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1411 868 moveto
-1442 844 1496 795 1496 738 curveto
-1496 738 1496 738 1496 450 curveto
-1496 370 1604 330 1661 314 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1661.88 317.393 moveto
-1671 312 lineto
-1660.51 310.529 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1661.88 317.393 moveto
-1671 312 lineto
-1660.51 310.529 lineto
-closepath stroke
-grestore
-% Indtypes
-gsave
-0.502 1.000 0.820 nodecolor
-539 1026 37.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-539 1026 37.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-539 1021 moveto 48 -0.5 (Indtypes) alignedtext
-grestore
-% Indtypes->Typeops
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 574 1020 moveto
-650 1008 831 977 915 962 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 915.881 965.393 moveto
-925 960 lineto
-914.508 958.529 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 915.881 965.393 moveto
-925 960 lineto
-914.508 958.529 lineto
-closepath stroke
-grestore
-% Type_errors
-gsave
-0.502 1.000 0.820 nodecolor
-713 810 47.1758 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-713 810 47.1758 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-713 805 moveto 69 -0.5 (Type_errors) alignedtext
-grestore
-% Inductive->Type_errors
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 813 868 moveto
-794 858 769 843 748 830 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 749.441 826.797 moveto
-739 825 lineto
-746.042 832.916 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 749.441 826.797 moveto
-739 825 lineto
-746.042 832.916 lineto
-closepath stroke
-grestore
-% Reduction
-gsave
-0.502 1.000 0.820 nodecolor
-713 738 41.1755 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-713 738 41.1755 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-713 733 moveto 57 -0.5 (Reduction) alignedtext
-grestore
-% Type_errors->Reduction
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 713 792 moveto
-713 784 713 775 713 766 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 716.5 766 moveto
-713 756 lineto
-709.5 766 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 716.5 766 moveto
-713 756 lineto
-709.5 766 lineto
-closepath stroke
-grestore
-% Modops
-gsave
-0.502 1.000 0.820 nodecolor
-1404 954 35.1752 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1404 954 35.1752 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1404 949 moveto 45 -0.5 (Modops) alignedtext
-grestore
-% Modops->Environ
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1439 951 moveto
-1511 943 1670 914 1670 810 curveto
-1670 810 1670 810 1670 738 curveto
-1670 639 1322 606 1194 597 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1194.3 593.512 moveto
-1184 596 lineto
-1193.6 600.478 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1194.3 593.512 moveto
-1184 596 lineto
-1193.6 600.478 lineto
-closepath stroke
-grestore
-% Modops->Entries
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1401 936 moveto
-1400 928 1398 919 1396 910 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1399.39 909.119 moveto
-1394 900 lineto
-1392.53 910.492 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1399.39 909.119 moveto
-1394 900 lineto
-1392.53 910.492 lineto
-closepath stroke
-grestore
-% Mod_typing
-gsave
-0.502 1.000 0.820 nodecolor
-1157 1170 47.1758 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1157 1170 47.1758 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1157 1165 moveto 69 -0.5 (Mod_typing) alignedtext
-grestore
-% Subtyping
-gsave
-0.502 1.000 0.820 nodecolor
-1404 1026 42.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1404 1026 42.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1404 1021 moveto 58 -0.5 (Subtyping) alignedtext
-grestore
-% Mod_typing->Subtyping
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1183 1155 moveto
-1227 1129 1320 1075 1370 1046 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1371.96 1048.92 moveto
-1379 1041 lineto
-1368.56 1042.8 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1371.96 1048.92 moveto
-1379 1041 lineto
-1368.56 1042.8 lineto
-closepath stroke
-grestore
-% Term_typing
-gsave
-0.502 1.000 0.820 nodecolor
-960 1098 50.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-960 1098 50.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-960 1093 moveto 74 -0.5 (Term_typing) alignedtext
-grestore
-% Mod_typing->Term_typing
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1123 1157 moveto
-1090 1145 1040 1127 1005 1114 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1005.58 1110.52 moveto
-995 1111 lineto
-1003.57 1117.23 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1005.58 1110.52 moveto
-995 1111 lineto
-1003.57 1117.23 lineto
-closepath stroke
-grestore
-% Subtyping->Typeops
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1365 1020 moveto
-1282 1007 1092 975 1005 962 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1005.49 958.529 moveto
-995 960 lineto
-1004.12 965.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1005.49 958.529 moveto
-995 960 lineto
-1004.12 965.393 lineto
-closepath stroke
-grestore
-% Subtyping->Modops
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1404 1008 moveto
-1404 1000 1404 991 1404 982 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1407.5 982 moveto
-1404 972 lineto
-1400.5 982 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1407.5 982 moveto
-1404 972 lineto
-1400.5 982 lineto
-closepath stroke
-grestore
-% Term_typing->Cooking
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 960 1080 moveto
-960 1072 960 1063 960 1054 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 963.5 1054 moveto
-960 1044 lineto
-956.5 1054 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 963.5 1054 moveto
-960 1044 lineto
-956.5 1054 lineto
-closepath stroke
-grestore
-% Term_typing->Indtypes
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 915 1090 moveto
-833 1077 665 1048 584 1034 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 584.492 1030.53 moveto
-574 1032 lineto
-583.119 1037.39 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 584.492 1030.53 moveto
-574 1032 lineto
-583.119 1037.39 lineto
-closepath stroke
-grestore
-% Reduction->Closure
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 713 720 moveto
-713 712 713 703 713 694 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 716.5 694 moveto
-713 684 lineto
-709.5 694 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 716.5 694 moveto
-713 684 lineto
-709.5 694 lineto
-closepath stroke
-grestore
-% Reduction->Conv_oracle
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 690 723 moveto
-633 686 482 587 415 544 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 417.1 541.2 moveto
-407 538 lineto
-412.9 546.8 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 417.1 541.2 moveto
-407 538 lineto
-412.9 546.8 lineto
-closepath stroke
-grestore
-% Safe_typing
-gsave
-0.502 1.000 0.820 nodecolor
-1157 1242 47.1777 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1157 1242 47.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1157 1237 moveto 68 -0.5 (Safe_typing) alignedtext
-grestore
-% Safe_typing->Mod_typing
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1157 1224 moveto
-1157 1216 1157 1207 1157 1198 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1160.5 1198 moveto
-1157 1188 lineto
-1153.5 1198 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1160.5 1198 moveto
-1157 1188 lineto
-1153.5 1198 lineto
-closepath stroke
-grestore
-% Univ->Names
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 555 84 moveto
-504 71 388 42 327 27 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 327.492 23.5292 moveto
-317 25 lineto
-326.119 30.3933 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 327.492 23.5292 moveto
-317 25 lineto
-326.119 30.3933 lineto
-closepath stroke
-grestore
-% Vconv
-gsave
-0.502 1.000 0.820 nodecolor
-1152 810 31.1748 18 ellipse_path fill
-0.393658 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-1152 810 31.1748 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-1152 805 moveto 37 -0.5 (Vconv) alignedtext
-grestore
-% Vconv->Csymtable
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1151 792 moveto
-1150 767 1149 723 1148 694 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 694 moveto
-1148 684 lineto
-1144.5 694 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 1151.5 694 moveto
-1148 684 lineto
-1144.5 694 lineto
-closepath stroke
-grestore
-% Vconv->Reduction
-gsave
-0.393658 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1122 805 moveto
-1047 792 852 760 761 746 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 761.492 742.529 moveto
-751 744 lineto
-760.119 749.393 lineto
-closepath fill
-0.393658 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 761.492 742.529 moveto
-751 744 lineto
-760.119 749.393 lineto
-closepath stroke
-grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-%%BoundingBox: 36 36 535 756
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll
deleted file mode 100644
index 059526d9..00000000
--- a/dev/ocamlweb-doc/lex.mll
+++ /dev/null
@@ -1,81 +0,0 @@
-
-{
- open Lexing
- open Syntax
-
- let chan_out = ref stdout
-
- let comment_depth = ref 0
- let print s = output_string !chan_out s
-
- exception Fin_fichier
-
-}
-
-let space = [' ' '\t' '\n']
-let letter = ['a'-'z' 'A'-'Z']
-let digit = ['0'-'9']
-
-let identifier = letter (letter | digit | ['_' '\''])*
-let number = digit+
-let oper = ['-' '+' '/' '*' '|' '>' '<' '=' '%' '#' '$' ':' '\\' '?'
- '.' '!' '@' ]+
-
-rule token = parse
- | "let" {LET}
- | "in" {IN}
- | "match" {MATCH}
- | "with" {WITH}
- | "end" {END}
- | "and" {AND}
- | "fun" {FUN}
- | "if" {IF}
- | "then" {THEN}
- | "else" {ELSE}
- | "eval" {EVAL}
- | "for" {FOR}
- | "Prop" {PROP}
- | "Set" {SET}
- | "Type" {TYPE}
- | "fix" {FIX}
- | "cofix" {COFIX}
- | "struct" {STRUCT}
- | "as" {AS}
-
- | "Simpl" {SIMPL}
-
- | "_" {WILDCARD}
- | "(" {LPAR}
- | ")" {RPAR}
- | "{" {LBRACE}
- | "}" {RBRACE}
- | "!" {BANG}
- | "@" {AT}
- | ":" {COLON}
- | ":=" {COLONEQ}
- | "." {DOT}
- | "," {COMMA}
- | "->" {OPER "->"}
- | "=>" {RARROW}
- | "|" {BAR}
- | "%" {PERCENT}
-
- | '?' { META(ident lexbuf)}
- | number { INT(Lexing.lexeme lexbuf) }
- | oper { OPER(Lexing.lexeme lexbuf) }
- | identifier { IDENT (Lexing.lexeme lexbuf) }
- | "(*" (*"*)"*) { comment_depth := 1;
- comment lexbuf;
- token lexbuf }
- | space+ { token lexbuf}
- | eof { EOF }
-
-and ident = parse
- | identifier { Lexing.lexeme lexbuf }
-
-and comment = parse
- | "(*" (*"*)"*) { incr comment_depth; comment lexbuf }
- | (*"(*"*) "*)"
- { decr comment_depth; if !comment_depth > 0 then comment lexbuf }
- | eof { raise Fin_fichier }
- | _ { comment lexbuf }
diff --git a/dev/ocamlweb-doc/library.dep.ps b/dev/ocamlweb-doc/library.dep.ps
deleted file mode 100644
index c9bb351e..00000000
--- a/dev/ocamlweb-doc/library.dep.ps
+++ /dev/null
@@ -1,773 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
-%%For: (notin) Jean-Marc Notin,,,
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: (atend)
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-EncodingVector 45 /hyphen put
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-setupLatin1
-%%Page: 1 1
-%%PageBoundingBox: 36 36 576 752
-%%PageOrientation: Landscape
-gsave
-36 36 576 752 boxprim clip newpath
-0 0 1 beginpage
-0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 544 lineto
-723 544 lineto
-723 -4 lineto
-closepath fill
-0.985401 setlinewidth
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 544 lineto
-723 544 lineto
-723 -4 lineto
-closepath stroke
-% Declare
-gsave
-0.502 1.000 0.820 nodecolor
-488 436 34.1751 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-488 436 34.1751 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-488 431 moveto 43 -0.5 (Declare) alignedtext
-grestore
-% Dischargedhypsmap
-gsave
-0.502 1.000 0.820 nodecolor
-488 353 69.1764 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-488 353 69.1764 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-488 348 moveto 113 -0.5 (Dischargedhypsmap) alignedtext
-grestore
-% Declare->Dischargedhypsmap
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 488 418 moveto
-488 407 488 393 488 381 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 491.5 381 moveto
-488 371 lineto
-484.5 381 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 491.5 381 moveto
-488 371 lineto
-484.5 381 lineto
-closepath stroke
-grestore
-% Impargs
-gsave
-0.502 1.000 0.820 nodecolor
-201 353 36.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-201 353 36.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-201 348 moveto 46 -0.5 (Impargs) alignedtext
-grestore
-% Declare->Impargs
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 458 427 moveto
-407 412 301 382 242 365 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 242.584 361.521 moveto
-232 362 lineto
-240.573 368.226 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 242.584 361.521 moveto
-232 362 lineto
-240.573 368.226 lineto
-closepath stroke
-grestore
-% Decl_kinds
-gsave
-0.502 1.000 0.820 nodecolor
-661 353 44.1757 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-661 353 44.1757 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-661 348 moveto 63 -0.5 (Decl_kinds) alignedtext
-grestore
-% Declare->Decl_kinds
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 514 424 moveto
-543 410 590 388 624 372 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 625.958 374.916 moveto
-633 367 lineto
-622.559 368.797 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 625.958 374.916 moveto
-633 367 lineto
-622.559 368.797 lineto
-closepath stroke
-grestore
-% Lib
-gsave
-0.502 1.000 0.820 nodecolor
-219 270 27 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-219 270 27 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-219 265 moveto 20 -0.5 (Lib) alignedtext
-grestore
-% Dischargedhypsmap->Lib
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 443 339 moveto
-390 323 302 296 254 281 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 254.584 277.521 moveto
-244 278 lineto
-252.573 284.226 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 254.584 277.521 moveto
-244 278 lineto
-252.573 284.226 lineto
-closepath stroke
-grestore
-% Global
-gsave
-0.502 1.000 0.820 nodecolor
-82 270 32.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-82 270 32.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-82 265 moveto 38 -0.5 (Global) alignedtext
-grestore
-% Impargs->Global
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 180 338 moveto
-161 325 132 305 110 290 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 112.1 287.2 moveto
-102 284 lineto
-107.9 292.8 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 112.1 287.2 moveto
-102 284 lineto
-107.9 292.8 lineto
-closepath stroke
-grestore
-% Impargs->Lib
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 205 335 moveto
-207 324 210 310 213 298 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 216.471 298.492 moveto
-215 288 lineto
-209.607 297.119 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 216.471 298.492 moveto
-215 288 lineto
-209.607 297.119 lineto
-closepath stroke
-grestore
-% Declaremods
-gsave
-0.502 1.000 0.820 nodecolor
-65 353 49.1759 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-65 353 49.1759 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-65 348 moveto 73 -0.5 (Declaremods) alignedtext
-grestore
-% Declaremods->Global
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 69 335 moveto
-71 324 74 310 76 298 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 79.4708 298.492 moveto
-78 288 lineto
-72.6067 297.119 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 79.4708 298.492 moveto
-78 288 lineto
-72.6067 297.119 lineto
-closepath stroke
-grestore
-% Declaremods->Lib
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 93 338 moveto
-120 324 161 301 189 286 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 190.958 288.916 moveto
-198 281 lineto
-187.559 282.797 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 190.958 288.916 moveto
-198 281 lineto
-187.559 282.797 lineto
-closepath stroke
-grestore
-% Summary
-gsave
-0.502 1.000 0.820 nodecolor
-69 103 40.1755 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-69 103 40.1755 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-69 98 moveto 55 -0.5 (Summary) alignedtext
-grestore
-% Global->Summary
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 81 252 moveto
-78 223 74 166 71 131 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 74.4778 130.602 moveto
-70 121 lineto
-67.5125 131.299 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 74.4778 130.602 moveto
-70 121 lineto
-67.5125 131.299 lineto
-closepath stroke
-grestore
-% Libnames
-gsave
-0.502 1.000 0.820 nodecolor
-203 103 40.1755 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-203 103 40.1755 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-203 98 moveto 55 -0.5 (Libnames) alignedtext
-grestore
-% Global->Libnames
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 94 253 moveto
-115 224 159 164 184 129 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 186.8 131.1 moveto
-190 121 lineto
-181.2 126.9 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 186.8 131.1 moveto
-190 121 lineto
-181.2 126.9 lineto
-closepath stroke
-grestore
-% Nametab
-gsave
-0.502 1.000 0.820 nodecolor
-203 186 38.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-203 186 38.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-203 181 moveto 50 -0.5 (Nametab) alignedtext
-grestore
-% Lib->Nametab
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 216 252 moveto
-214 241 211 226 209 214 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 212.393 213.119 moveto
-207 204 lineto
-205.529 214.492 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 212.393 213.119 moveto
-207 204 lineto
-205.529 214.492 lineto
-closepath stroke
-grestore
-% Libobject
-gsave
-0.502 1.000 0.820 nodecolor
-329 186 40.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-329 186 40.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-329 181 moveto 54 -0.5 (Libobject) alignedtext
-grestore
-% Lib->Libobject
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 237 256 moveto
-254 243 280 223 300 208 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 302.1 210.8 moveto
-308 202 lineto
-297.9 205.2 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 302.1 210.8 moveto
-308 202 lineto
-297.9 205.2 lineto
-closepath stroke
-grestore
-% Nameops
-gsave
-0.502 1.000 0.820 nodecolor
-203 20 39.1777 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-203 20 39.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-203 15 moveto 52 -0.5 (Nameops) alignedtext
-grestore
-% Libnames->Nameops
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 203 85 moveto
-203 74 203 60 203 48 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 206.5 48 moveto
-203 38 lineto
-199.5 48 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 206.5 48 moveto
-203 38 lineto
-199.5 48 lineto
-closepath stroke
-grestore
-% Goptions
-gsave
-0.502 1.000 0.820 nodecolor
-322 353 38.1754 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-322 353 38.1754 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-322 348 moveto 51 -0.5 (Goptions) alignedtext
-grestore
-% Goptions->Lib
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 303 337 moveto
-287 324 263 305 245 291 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 246.831 287.951 moveto
-237 284 lineto
-242.221 293.219 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 246.831 287.951 moveto
-237 284 lineto
-242.221 293.219 lineto
-closepath stroke
-grestore
-% Nametab->Summary
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 180 172 moveto
-158 159 125 138 101 123 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 102.441 119.797 moveto
-92 118 lineto
-99.0418 125.916 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 102.441 119.797 moveto
-92 118 lineto
-99.0418 125.916 lineto
-closepath stroke
-grestore
-% Nametab->Libnames
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 203 168 moveto
-203 157 203 143 203 131 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 206.5 131 moveto
-203 121 lineto
-199.5 131 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 206.5 131 moveto
-203 121 lineto
-199.5 131 lineto
-closepath stroke
-grestore
-% Libobject->Libnames
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 306 171 moveto
-286 158 256 138 235 124 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 236.262 120.635 moveto
-226 118 lineto
-232.379 126.459 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 236.262 120.635 moveto
-226 118 lineto
-232.379 126.459 lineto
-closepath stroke
-grestore
-% Library
-gsave
-0.502 1.000 0.820 nodecolor
-65 436 34.1751 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-65 436 34.1751 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-65 431 moveto 43 -0.5 (Library) alignedtext
-grestore
-% Library->Declaremods
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 65 418 moveto
-65 407 65 393 65 381 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 68.5001 381 moveto
-65 371 lineto
-61.5001 381 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 68.5001 381 moveto
-65 371 lineto
-61.5001 381 lineto
-closepath stroke
-grestore
-% States
-gsave
-0.502 1.000 0.820 nodecolor
-65 519 29.1747 18 ellipse_path fill
-0.985401 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-65 519 29.1747 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-65 514 moveto 33 -0.5 (States) alignedtext
-grestore
-% States->Library
-gsave
-0.985401 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 65 501 moveto
-65 490 65 476 65 464 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 68.5001 464 moveto
-65 454 lineto
-61.5001 464 lineto
-closepath fill
-0.985401 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 68.5001 464 moveto
-65 454 lineto
-61.5001 464 lineto
-closepath stroke
-grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-%%BoundingBox: 36 36 576 752
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/macros.tex b/dev/ocamlweb-doc/macros.tex
deleted file mode 100644
index 6beacf7b..00000000
--- a/dev/ocamlweb-doc/macros.tex
+++ /dev/null
@@ -1,7 +0,0 @@
-
-% macros for coq.tex
-
-\newcommand{\Coq}{\textsf{Coq}}
-\newcommand{\CCI}{Calculus of Inductive Constructions}
-
-\newcommand{\refsec}[1]{\textbf{\ref{#1}}} \ No newline at end of file
diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml
deleted file mode 100644
index b145fffd..00000000
--- a/dev/ocamlweb-doc/parse.ml
+++ /dev/null
@@ -1,183 +0,0 @@
-
-open Ast
-
-type assoc = L | R | N
-
-let level = function
- | "--" -> 70,L
- | "=" -> 70,N
- | "+" -> 60,L
- | "++" -> 60,R
- | "+++" -> 60,R
- | "-" -> 60,L
- | "*" -> 50,L
- | "/" -> 50,L
- | "**" -> 40,R
- | ":" -> (100,R)
- | "->" -> (90,R)
- | s -> failwith ("unknowm operator '"^s^"'")
-
-let fixity = function
- | "--" -> [L]
- | "=" -> [N]
- | ("+"|"-"|"*"|"/") -> [L;N]
- | "++" -> [R]
- | _ -> [L;N;R]
-
-let ground_oper = function
- ("-"|"+") -> true
- | _ -> false
-
-let is_prefix op = List.mem L (fixity op)
-let is_infix op = List.mem N (fixity op)
-let is_postfix op = List.mem R (fixity op)
-
-let mk_inf op t1 t2 =
- if not (is_infix op) then failwith (op^" not infix");
- Infix(op,t1,t2)
-
-let mk_post op t =
- if not (is_postfix op) then failwith (op^" not postfix");
- Postfix(op,t)
-
-
-(* Pb avec ground_oper: pas de diff entre -1 et -(1) *)
-let mk_pre op t =
- if not (is_prefix op) then failwith (op^" not prefix");
- if ground_oper op then
- match t with
- | Int i -> Int (op^i)
- | _ -> Prefix(op,t)
- else Prefix(op,t)
-
-(* teste si on peut reduire op suivi d'un op de niveau (n,a)
- si la reponse est false, c'est que l'op (n,a) doit se reduire
- avant *)
-let red_left_op (nl,al) (nr,ar) =
- if nl < nr then true
- else
- if nl = nr then
- match al,ar with
- | (L|N), L -> true
- | R, (R|N) -> false
- | R, L -> failwith "conflit d'assoc: ambigu"
- | (L|N), (R|N) -> failwith "conflit d'assoc: blocage"
- else false
-
-
-type level = int * assoc
-type stack =
- | PrefixOper of string list
- | Term of constr_ast * stack
- | Oper of string list * string * constr_ast * stack
-
-let rec str_ast = function
- | Infix(op,t1,t2) -> str_ast t1 ^ " " ^ op ^ " " ^ str_ast t2
- | Postfix(op,t) -> str_ast t ^ " " ^ op
- | Prefix(op,t) -> op ^ " " ^ str_ast t
- | _ -> "_"
-
-let rec str_stack = function
- | PrefixOper ops -> String.concat " " (List.rev ops)
- | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")"
- | Oper(ops,lop,t,s) ->
- str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^
- String.concat " " (List.rev ops)
-
-let pps s = prerr_endline (str_stack s)
-let err s stk = failwith (s^": "^str_stack stk)
-
-
-let empty = PrefixOper []
-
-let check_fixity_term stk =
- match stk with
- Term _ -> err "2 termes successifs" stk
- | _ -> ()
-
-let shift_term t stk =
- check_fixity_term stk;
- Term(t,stk)
-
-let shift_oper op stk =
- match stk with
- | Oper(ops,lop,t,s) -> Oper(op::ops,lop,t,s)
- | Term(t,s) -> Oper([],op,t,s)
- | PrefixOper ops -> PrefixOper (op::ops)
-
-let is_reducible lv stk =
- match stk with
- | Oper([],iop,_,_) -> red_left_op (level iop) lv
- | Oper(op::_,_,_,_) -> red_left_op (level op) lv
- | PrefixOper(op::_) -> red_left_op (level op) lv
- | _ -> false
-
-let reduce_head (t,stk) =
- match stk with
- | Oper([],iop,t1,s) ->
- (Infix(iop,t1,t), s)
- | Oper(op::ops,lop,t',s) ->
- (mk_pre op t, Oper(ops,lop,t',s))
- | PrefixOper(op::ops) ->
- (Prefix(op,t), PrefixOper ops)
- | _ -> assert false
-
-let rec reduce_level lv (t,s) =
- if is_reducible lv s then reduce_level lv (reduce_head (t, s))
- else (t, s)
-
-let reduce_post op (t,s) =
- let (t',s') = reduce_level (level op) (t,s) in
- (mk_post op t', s')
-
-let reduce_posts stk =
- match stk with
- Oper(ops,iop,t,s) ->
- let pts1 = reduce_post iop (t,s) in
- List.fold_right reduce_post ops pts1
- | Term(t,s) -> (t,s)
- | PrefixOper _ -> failwith "reduce_posts"
-
-
-let shift_infix op stk =
- let (t,s) = reduce_level (level op) (reduce_posts stk) in
- Oper([],op,t,s)
-
-let is_better_infix op stk =
- match stk with
- | Oper(ops,iop,t,s) ->
- is_postfix iop &&
- List.for_all is_postfix ops &&
- (not (is_prefix op) || red_left_op (level iop) (level op))
- | Term _ -> false
- | _ -> assert false
-
-let parse_oper op stk =
- match stk with
- | PrefixOper _ ->
- if is_prefix op then shift_oper op stk else failwith "prefix_oper"
- | Oper _ ->
- if is_infix op then
- if is_better_infix op stk then shift_infix op stk
- else shift_oper op stk
- else if is_prefix op then shift_oper op stk
- else if is_postfix op then
- let (t,s) = reduce_post op (reduce_posts stk) in
- Term(t,s)
- else assert false
- | Term(t,s) ->
- if is_infix op then shift_infix op stk
- else if is_postfix op then
- let (t2,s2) = reduce_post op (t,s) in Term(t2,s2)
- else failwith "infix/postfix"
-
-let parse_term = shift_term
-
-let rec close_stack stk =
- match stk with
- Term(t,PrefixOper []) -> t
- | PrefixOper _ -> failwith "expression sans atomes"
- | _ ->
- let (t,s) = reduce_head (reduce_posts stk) in
- close_stack (Term(t,s))
-
diff --git a/dev/ocamlweb-doc/parsing.dep.ps b/dev/ocamlweb-doc/parsing.dep.ps
deleted file mode 100644
index 723d8c69..00000000
--- a/dev/ocamlweb-doc/parsing.dep.ps
+++ /dev/null
@@ -1,1115 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: 35 35 577 314
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
- dup 306 /AE
- dup 301 /Aacute
- dup 302 /Acircumflex
- dup 304 /Adieresis
- dup 300 /Agrave
- dup 305 /Aring
- dup 303 /Atilde
- dup 307 /Ccedilla
- dup 311 /Eacute
- dup 312 /Ecircumflex
- dup 313 /Edieresis
- dup 310 /Egrave
- dup 315 /Iacute
- dup 316 /Icircumflex
- dup 317 /Idieresis
- dup 314 /Igrave
- dup 334 /Udieresis
- dup 335 /Yacute
- dup 376 /thorn
- dup 337 /germandbls
- dup 341 /aacute
- dup 342 /acircumflex
- dup 344 /adieresis
- dup 346 /ae
- dup 340 /agrave
- dup 345 /aring
- dup 347 /ccedilla
- dup 351 /eacute
- dup 352 /ecircumflex
- dup 353 /edieresis
- dup 350 /egrave
- dup 355 /iacute
- dup 356 /icircumflex
- dup 357 /idieresis
- dup 354 /igrave
- dup 360 /dcroat
- dup 361 /ntilde
- dup 363 /oacute
- dup 364 /ocircumflex
- dup 366 /odieresis
- dup 362 /ograve
- dup 365 /otilde
- dup 370 /oslash
- dup 372 /uacute
- dup 373 /ucircumflex
- dup 374 /udieresis
- dup 371 /ugrave
- dup 375 /yacute
- dup 377 /ydieresis
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- dup scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-%%Page: 1 1
-%%PageBoundingBox: 36 36 577 314
-%%PageOrientation: Portrait
-gsave
-35 35 542 279 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0.6027 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-% Pcoq
-gsave 10 dict begin
-557 280 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-543 275 moveto
-(Pcoq)
-[7.68 6.24 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Extend
-gsave 10 dict begin
-664 226 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-643 221 moveto
-(Extend)
-[8.4 6.96 3.84 6.24 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Pcoq -> Extend
-newpath 579 269 moveto
-593 261 613 252 630 243 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 632 246 moveto
-639 238 lineto
-629 240 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 632 246 moveto
-639 238 lineto
-629 240 lineto
-closepath
-stroke
-end grestore
-
-% Ast
-gsave 10 dict begin
-764 172 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-753 167 moveto
-(Ast)
-[10.08 5.28 3.84]
-xshow
-end grestore
-end grestore
-
-% Extend -> Ast
-newpath 688 213 moveto
-701 206 719 196 734 188 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 736 191 moveto
-743 183 lineto
-733 185 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 736 191 moveto
-743 183 lineto
-733 185 lineto
-closepath
-stroke
-end grestore
-
-% Lexer
-gsave 10 dict begin
-764 226 29 18 ellipse_path
-stroke
-gsave 10 dict begin
-747 221 moveto
-(Lexer)
-[8.4 5.76 6.48 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-% Extend -> Lexer
-newpath 698 226 moveto
-706 226 715 226 724 226 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 724 230 moveto
-734 226 lineto
-724 223 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 724 230 moveto
-734 226 lineto
-724 223 lineto
-closepath
-stroke
-end grestore
-
-% Termast
-gsave 10 dict begin
-557 172 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-534 167 moveto
-(Termast)
-[7.2 6.24 4.8 10.8 6.24 5.28 3.84]
-xshow
-end grestore
-end grestore
-
-% Termast -> Ast
-newpath 593 172 moveto
-630 172 689 172 727 172 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 727 176 moveto
-737 172 lineto
-727 169 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 727 176 moveto
-737 172 lineto
-727 169 lineto
-closepath
-stroke
-end grestore
-
-% Coqast
-gsave 10 dict begin
-863 172 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-843 167 moveto
-(Coqast)
-[9.36 6.96 6.96 6.24 5.28 3.84]
-xshow
-end grestore
-end grestore
-
-% Ast -> Coqast
-newpath 791 172 moveto
-800 172 810 172 820 172 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 820 176 moveto
-830 172 lineto
-820 169 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 820 176 moveto
-830 172 lineto
-820 169 lineto
-closepath
-stroke
-end grestore
-
-% Tactic_printer
-gsave 10 dict begin
-53 126 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 121 moveto
-(Tactic_printer)
-[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 4.8 3.84 6.96 3.84 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-% Pptactic
-gsave 10 dict begin
-178 126 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-155 121 moveto
-(Pptactic)
-[7.68 6.96 4.08 6.24 6.24 3.84 3.84 6.24]
-xshow
-end grestore
-end grestore
-
-% Tactic_printer -> Pptactic
-newpath 106 126 moveto
-114 126 123 126 132 126 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 132 130 moveto
-142 126 lineto
-132 123 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 132 130 moveto
-142 126 lineto
-132 123 lineto
-closepath
-stroke
-end grestore
-
-% Printer
-gsave 10 dict begin
-289 72 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-269 67 moveto
-(Printer)
-[7.68 4.8 3.84 6.96 3.84 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-% Pptactic -> Printer
-newpath 204 113 moveto
-219 105 238 96 255 88 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 256 91 moveto
-264 84 lineto
-253 85 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 256 91 moveto
-264 84 lineto
-253 85 lineto
-closepath
-stroke
-end grestore
-
-% Search
-gsave 10 dict begin
-178 72 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-159 67 moveto
-(Search)
-[7.68 6.24 6.24 4.56 6 6.96]
-xshow
-end grestore
-end grestore
-
-% Search -> Printer
-newpath 210 72 moveto
-221 72 234 72 246 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 246 76 moveto
-256 72 lineto
-246 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 246 76 moveto
-256 72 lineto
-246 69 lineto
-closepath
-stroke
-end grestore
-
-% Printer -> Termast
-newpath 316 62 moveto
-355 48 430 30 484 58 curveto
-518 77 538 117 548 144 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 545 146 moveto
-552 154 lineto
-552 143 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 545 146 moveto
-552 154 lineto
-552 143 lineto
-closepath
-stroke
-end grestore
-
-% Esyntax
-gsave 10 dict begin
-557 226 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-533 221 moveto
-(Esyntax)
-[8.4 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% Printer -> Esyntax
-newpath 322 71 moveto
-370 70 460 72 484 91 curveto
-489 95 516 193 520 197 curveto
-527 204 532 203 538 204 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 536 207 moveto
-547 208 lineto
-539 201 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 536 207 moveto
-547 208 lineto
-539 201 lineto
-closepath
-stroke
-end grestore
-
-% Ppconstr
-gsave 10 dict begin
-424 388 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-399 383 moveto
-(Ppconstr)
-[7.68 6.96 6.24 6.96 6.96 5.28 3.84 4.56]
-xshow
-end grestore
-end grestore
-
-% Printer -> Ppconstr
-newpath 292 90 moveto
-300 147 329 319 364 361 curveto
-369 367 375 371 382 375 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 380 378 moveto
-391 379 lineto
-383 372 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 380 378 moveto
-391 379 lineto
-383 372 lineto
-closepath
-stroke
-end grestore
-
-% Esyntax -> Extend
-newpath 594 226 moveto
-602 226 611 226 620 226 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 620 230 moveto
-630 226 lineto
-620 223 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 620 230 moveto
-630 226 lineto
-620 223 lineto
-closepath
-stroke
-end grestore
-
-% Ppconstr -> Pcoq
-newpath 454 377 moveto
-464 373 475 368 484 361 curveto
-506 345 526 322 540 304 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 543 306 moveto
-546 296 lineto
-537 302 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 543 306 moveto
-546 296 lineto
-537 302 lineto
-closepath
-stroke
-end grestore
-
-% Prettyp
-gsave 10 dict begin
-178 18 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-158 13 moveto
-(Prettyp)
-[7.68 4.56 6 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Prettyp -> Printer
-newpath 203 30 moveto
-218 38 238 47 255 55 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 254 58 moveto
-264 60 lineto
-257 52 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 254 58 moveto
-264 60 lineto
-257 52 lineto
-closepath
-stroke
-end grestore
-
-% Printmod
-gsave 10 dict begin
-289 18 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-263 13 moveto
-(Printmod)
-[7.68 4.8 3.84 6.96 3.84 10.8 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Prettyp -> Printmod
-newpath 211 18 moveto
-220 18 230 18 240 18 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 240 22 moveto
-250 18 lineto
-240 15 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 240 22 moveto
-250 18 lineto
-240 15 lineto
-closepath
-stroke
-end grestore
-
-% G_zsyntax
-gsave 10 dict begin
-424 172 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-393 167 moveto
-(G_zsyntax)
-[10.08 6.96 6.24 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% G_zsyntax -> Pcoq
-newpath 458 183 moveto
-467 188 476 193 484 199 curveto
-507 218 501 233 520 253 curveto
-523 256 526 259 530 261 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 528 264 moveto
-538 267 lineto
-532 258 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 528 264 moveto
-538 267 lineto
-532 258 lineto
-closepath
-stroke
-end grestore
-
-% G_zsyntax -> Termast
-newpath 468 172 moveto
-482 172 497 172 511 172 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 511 176 moveto
-521 172 lineto
-511 169 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 511 176 moveto
-521 172 lineto
-511 169 lineto
-closepath
-stroke
-end grestore
-
-% G_zsyntax -> Esyntax
-newpath 455 185 moveto
-474 193 499 203 520 211 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 518 214 moveto
-529 215 lineto
-521 208 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 518 214 moveto
-529 215 lineto
-521 208 lineto
-closepath
-stroke
-end grestore
-
-% G_string_syntax
-gsave 10 dict begin
-424 280 59 18 ellipse_path
-stroke
-gsave 10 dict begin
-377 275 moveto
-(G_string_syntax)
-[10.08 6.96 5.28 3.84 4.8 3.84 6.96 6.96 6.96 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% G_string_syntax -> Pcoq
-newpath 484 280 moveto
-496 280 509 280 520 280 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 520 284 moveto
-530 280 lineto
-520 277 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 520 284 moveto
-530 280 lineto
-520 277 lineto
-closepath
-stroke
-end grestore
-
-% G_string_syntax -> Esyntax
-newpath 460 266 moveto
-478 258 501 249 520 242 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 521 245 moveto
-529 238 lineto
-518 239 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 521 245 moveto
-529 238 lineto
-518 239 lineto
-closepath
-stroke
-end grestore
-
-% G_rsyntax
-gsave 10 dict begin
-424 118 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-394 113 moveto
-(G_rsyntax)
-[10.08 6.96 4.56 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% G_rsyntax -> Pcoq
-newpath 459 128 moveto
-468 132 477 138 484 145 curveto
-518 183 491 213 520 253 curveto
-523 256 526 259 529 262 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 527 265 moveto
-537 268 lineto
-531 259 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 527 265 moveto
-537 268 lineto
-531 259 lineto
-closepath
-stroke
-end grestore
-
-% G_rsyntax -> Termast
-newpath 455 131 moveto
-474 139 499 149 520 157 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 518 160 moveto
-529 161 lineto
-521 154 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 518 160 moveto
-529 161 lineto
-521 154 lineto
-closepath
-stroke
-end grestore
-
-% G_rsyntax -> Esyntax
-newpath 457 129 moveto
-467 133 476 139 484 145 curveto
-507 164 501 179 520 199 curveto
-522 201 525 203 527 205 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 525 208 moveto
-535 212 lineto
-530 203 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 525 208 moveto
-535 212 lineto
-530 203 lineto
-closepath
-stroke
-end grestore
-
-% G_natsyntax
-gsave 10 dict begin
-424 226 48 18 ellipse_path
-stroke
-gsave 10 dict begin
-388 221 moveto
-(G_natsyntax)
-[10.08 6.96 6.96 6.24 3.84 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% G_natsyntax -> Pcoq
-newpath 457 239 moveto
-478 248 504 259 525 266 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 523 269 moveto
-534 270 lineto
-526 263 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 523 269 moveto
-534 270 lineto
-526 263 lineto
-closepath
-stroke
-end grestore
-
-% G_natsyntax -> Termast
-newpath 457 213 moveto
-476 205 500 195 520 187 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 521 190 moveto
-529 183 lineto
-518 184 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 521 190 moveto
-529 183 lineto
-518 184 lineto
-closepath
-stroke
-end grestore
-
-% G_natsyntax -> Esyntax
-newpath 473 226 moveto
-485 226 498 226 510 226 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 510 230 moveto
-520 226 lineto
-510 223 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 510 230 moveto
-520 226 lineto
-510 223 lineto
-closepath
-stroke
-end grestore
-
-% G_ascii_syntax
-gsave 10 dict begin
-424 334 56 18 ellipse_path
-stroke
-gsave 10 dict begin
-380 329 moveto
-(G_ascii_syntax)
-[10.08 6.96 6.24 5.52 6.24 3.84 3.84 6.96 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% G_ascii_syntax -> Pcoq
-newpath 459 320 moveto
-479 311 504 301 525 293 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 526 296 moveto
-534 289 lineto
-523 290 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 526 296 moveto
-534 289 lineto
-523 290 lineto
-closepath
-stroke
-end grestore
-
-% G_ascii_syntax -> Esyntax
-newpath 462 321 moveto
-470 317 478 312 484 307 curveto
-507 288 501 273 520 253 curveto
-522 251 524 249 527 247 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 529 250 moveto
-535 241 lineto
-525 244 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 529 250 moveto
-535 241 lineto
-525 244 lineto
-closepath
-stroke
-end grestore
-
-% Egrammar
-gsave 10 dict begin
-424 442 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-394 437 moveto
-(Egrammar)
-[8.4 7.2 4.56 6.24 10.8 10.8 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-% Egrammar -> Pcoq
-newpath 458 431 moveto
-467 427 477 422 484 415 curveto
-516 385 537 337 548 308 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 551 309 moveto
-551 298 lineto
-545 307 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 551 309 moveto
-551 298 lineto
-545 307 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/preamble.tex b/dev/ocamlweb-doc/preamble.tex
deleted file mode 100644
index 2cd21f02..00000000
--- a/dev/ocamlweb-doc/preamble.tex
+++ /dev/null
@@ -1,8 +0,0 @@
-\documentclass[11pt]{article}
-\usepackage[latin1]{inputenc}
-\usepackage[T1]{fontenc}
-\usepackage{ocamlweb}
-\pagestyle{ocamlweb}
-\usepackage{fullpage}
-\usepackage{epsfig}
-\begin{document}
diff --git a/dev/ocamlweb-doc/pretyping.dep.ps b/dev/ocamlweb-doc/pretyping.dep.ps
deleted file mode 100644
index 02d1b8b5..00000000
--- a/dev/ocamlweb-doc/pretyping.dep.ps
+++ /dev/null
@@ -1,1259 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: 35 35 577 146
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
- dup 306 /AE
- dup 301 /Aacute
- dup 302 /Acircumflex
- dup 304 /Adieresis
- dup 300 /Agrave
- dup 305 /Aring
- dup 303 /Atilde
- dup 307 /Ccedilla
- dup 311 /Eacute
- dup 312 /Ecircumflex
- dup 313 /Edieresis
- dup 310 /Egrave
- dup 315 /Iacute
- dup 316 /Icircumflex
- dup 317 /Idieresis
- dup 314 /Igrave
- dup 334 /Udieresis
- dup 335 /Yacute
- dup 376 /thorn
- dup 337 /germandbls
- dup 341 /aacute
- dup 342 /acircumflex
- dup 344 /adieresis
- dup 346 /ae
- dup 340 /agrave
- dup 345 /aring
- dup 347 /ccedilla
- dup 351 /eacute
- dup 352 /ecircumflex
- dup 353 /edieresis
- dup 350 /egrave
- dup 355 /iacute
- dup 356 /icircumflex
- dup 357 /idieresis
- dup 354 /igrave
- dup 360 /dcroat
- dup 361 /ntilde
- dup 363 /oacute
- dup 364 /ocircumflex
- dup 366 /odieresis
- dup 362 /ograve
- dup 365 /otilde
- dup 370 /oslash
- dup 372 /uacute
- dup 373 /ucircumflex
- dup 374 /udieresis
- dup 371 /ugrave
- dup 375 /yacute
- dup 377 /ydieresis
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- dup scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-%%Page: 1 1
-%%PageBoundingBox: 36 36 577 146
-%%PageOrientation: Portrait
-gsave
-35 35 542 111 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0.3600 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-% Unification
-gsave 10 dict begin
-610 118 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-577 113 moveto
-(Unification)
-[9.6 6.96 3.84 4.8 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Evarutil
-gsave 10 dict begin
-728 72 36 18 ellipse_path
-stroke
-gsave 10 dict begin
-705 67 moveto
-(Evarutil)
-[8.4 6.72 6.24 4.8 6.96 3.84 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-% Unification -> Evarutil
-newpath 643 105 moveto
-657 99 674 93 689 87 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 691 90 moveto
-699 83 lineto
-688 83 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 691 90 moveto
-699 83 lineto
-688 83 lineto
-closepath
-stroke
-end grestore
-
-% Pattern
-gsave 10 dict begin
-728 210 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-708 205 moveto
-(Pattern)
-[7.44 6.24 3.84 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-% Unification -> Pattern
-newpath 631 134 moveto
-650 150 680 173 701 189 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 699 192 moveto
-709 195 lineto
-703 186 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 699 192 moveto
-709 195 lineto
-703 186 lineto
-closepath
-stroke
-end grestore
-
-% Retyping
-gsave 10 dict begin
-839 118 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-813 113 moveto
-(Retyping)
-[9.12 6 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Unification -> Retyping
-newpath 656 118 moveto
-695 118 750 118 790 118 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 790 122 moveto
-800 118 lineto
-790 115 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 790 122 moveto
-800 118 lineto
-790 115 lineto
-closepath
-stroke
-end grestore
-
-% Typing
-gsave 10 dict begin
-839 64 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-819 59 moveto
-(Typing)
-[6.96 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Evarutil -> Typing
-newpath 764 69 moveto
-775 68 786 67 797 67 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 797 70 moveto
-807 66 lineto
-797 64 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 797 70 moveto
-807 66 lineto
-797 64 lineto
-closepath
-stroke
-end grestore
-
-% Rawterm
-gsave 10 dict begin
-1109 110 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-1083 105 moveto
-(Rawterm)
-[9.36 5.76 10.08 3.84 6.24 4.8 10.8]
-xshow
-end grestore
-end grestore
-
-% Pattern -> Rawterm
-newpath 759 216 moveto
-816 226 939 239 1024 191 curveto
-1049 176 1038 155 1060 138 curveto
-1069 131 1077 130 1084 129 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1085 132 moveto
-1094 127 lineto
-1084 126 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1085 132 moveto
-1094 127 lineto
-1084 126 lineto
-closepath
-stroke
-end grestore
-
-% Inductiveops
-gsave 10 dict begin
-1109 164 49 18 ellipse_path
-stroke
-gsave 10 dict begin
-1073 159 moveto
-(Inductiveops)
-[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% Retyping -> Inductiveops
-newpath 878 120 moveto
-915 122 974 126 1024 137 curveto
-1037 139 1051 144 1064 148 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1063 151 moveto
-1074 151 lineto
-1065 145 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1063 151 moveto
-1074 151 lineto
-1065 145 lineto
-closepath
-stroke
-end grestore
-
-% Pretype_errors
-gsave 10 dict begin
-969 72 54 18 ellipse_path
-stroke
-gsave 10 dict begin
-927 67 moveto
-(Pretype_errors)
-[7.68 4.56 6 3.84 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52]
-xshow
-end grestore
-end grestore
-
-% Typing -> Pretype_errors
-newpath 871 66 moveto
-881 67 893 68 905 68 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 905 71 moveto
-915 69 lineto
-905 65 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 905 71 moveto
-915 69 lineto
-905 65 lineto
-closepath
-stroke
-end grestore
-
-% Pretype_errors -> Inductiveops
-newpath 998 87 moveto
-1007 92 1016 98 1024 104 curveto
-1042 116 1043 124 1060 137 curveto
-1063 139 1067 142 1071 144 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1070 147 moveto
-1080 149 lineto
-1073 141 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1070 147 moveto
-1080 149 lineto
-1073 141 lineto
-closepath
-stroke
-end grestore
-
-% Pretype_errors -> Rawterm
-newpath 1011 84 moveto
-1029 88 1048 94 1065 98 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1064 101 moveto
-1075 101 lineto
-1066 95 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1064 101 moveto
-1075 101 lineto
-1066 95 lineto
-closepath
-stroke
-end grestore
-
-% Tacred
-gsave 10 dict begin
-728 18 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-709 13 moveto
-(Tacred)
-[7.44 6.24 6.24 4.56 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% Tacred -> Retyping
-newpath 748 32 moveto
-754 36 759 41 764 45 curveto
-783 63 782 73 800 91 curveto
-802 93 805 95 808 97 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 806 100 moveto
-816 103 lineto
-810 94 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 806 100 moveto
-816 103 lineto
-810 94 lineto
-closepath
-stroke
-end grestore
-
-% Tacred -> Typing
-newpath 754 29 moveto
-769 35 787 43 803 49 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 802 53 moveto
-813 53 lineto
-805 46 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 802 53 moveto
-813 53 lineto
-805 46 lineto
-closepath
-stroke
-end grestore
-
-% Cbv
-gsave 10 dict begin
-1246 41 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-1234 36 moveto
-(Cbv)
-[9.36 6.48 6.96]
-xshow
-end grestore
-end grestore
-
-% Tacred -> Cbv
-newpath 760 19 moveto
-852 23 1111 35 1209 40 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1209 44 moveto
-1219 40 lineto
-1209 37 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1209 44 moveto
-1219 40 lineto
-1209 37 lineto
-closepath
-stroke
-end grestore
-
-% Evd
-gsave 10 dict begin
-1361 110 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-1349 105 moveto
-(Evd)
-[8.4 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Cbv -> Evd
-newpath 1266 53 moveto
-1284 64 1312 80 1332 93 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1331 96 moveto
-1341 98 lineto
-1334 90 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1331 96 moveto
-1341 98 lineto
-1334 90 lineto
-closepath
-stroke
-end grestore
-
-% Reductionops
-gsave 10 dict begin
-1246 164 51 18 ellipse_path
-stroke
-gsave 10 dict begin
-1207 159 moveto
-(Reductionops)
-[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% Inductiveops -> Reductionops
-newpath 1158 164 moveto
-1167 164 1175 164 1184 164 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1184 168 moveto
-1194 164 lineto
-1184 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1184 168 moveto
-1194 164 lineto
-1184 161 lineto
-closepath
-stroke
-end grestore
-
-% Reductionops -> Evd
-newpath 1277 150 moveto
-1294 142 1313 133 1330 125 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1331 128 moveto
-1339 121 lineto
-1328 122 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1331 128 moveto
-1339 121 lineto
-1328 122 lineto
-closepath
-stroke
-end grestore
-
-% Termops
-gsave 10 dict begin
-1462 110 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-1437 105 moveto
-(Termops)
-[7.2 6.24 4.8 10.8 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% Evd -> Termops
-newpath 1388 110 moveto
-1396 110 1405 110 1414 110 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1414 114 moveto
-1424 110 lineto
-1414 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1414 114 moveto
-1424 110 lineto
-1414 107 lineto
-closepath
-stroke
-end grestore
-
-% Recordops
-gsave 10 dict begin
-485 24 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-455 19 moveto
-(Recordops)
-[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% Classops
-gsave 10 dict begin
-610 20 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-584 15 moveto
-(Classops)
-[9.36 3.84 6.24 5.52 5.52 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% Recordops -> Classops
-newpath 528 23 moveto
-538 22 550 22 561 22 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 561 25 moveto
-571 21 lineto
-561 19 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 561 25 moveto
-571 21 lineto
-561 19 lineto
-closepath
-stroke
-end grestore
-
-% Classops -> Tacred
-newpath 649 19 moveto
-661 19 674 19 686 19 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 686 23 moveto
-696 19 lineto
-686 16 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 686 23 moveto
-696 19 lineto
-686 16 lineto
-closepath
-stroke
-end grestore
-
-% Rawterm -> Evd
-newpath 1148 110 moveto
-1196 110 1277 110 1324 110 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1324 114 moveto
-1334 110 lineto
-1324 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1324 114 moveto
-1334 110 lineto
-1324 107 lineto
-closepath
-stroke
-end grestore
-
-% Pretyping
-gsave 10 dict begin
-40 183 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 178 moveto
-(Pretyping)
-[7.68 4.56 6 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Pretyping -> Pattern
-newpath 78 189 moveto
-121 194 191 202 251 202 curveto
-251 202 251 202 485 202 curveto
-556 202 636 205 685 208 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 685 212 moveto
-695 208 lineto
-685 205 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 685 212 moveto
-695 208 lineto
-685 205 lineto
-closepath
-stroke
-end grestore
-
-% Cases
-gsave 10 dict begin
-146 64 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-129 59 moveto
-(Cases)
-[9.36 6.24 5.52 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-% Pretyping -> Cases
-newpath 53 166 moveto
-68 147 93 115 116 91 curveto
-118 89 119 88 121 86 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 124 88 moveto
-129 79 lineto
-119 83 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 124 88 moveto
-129 79 lineto
-119 83 lineto
-closepath
-stroke
-end grestore
-
-% Detyping
-gsave 10 dict begin
-969 164 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-942 159 moveto
-(Detyping)
-[10.08 6 3.84 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Pretyping -> Detyping
-newpath 78 177 moveto
-121 172 191 164 251 164 curveto
-251 164 251 164 728 164 curveto
-794 164 870 164 919 164 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 919 168 moveto
-929 164 lineto
-919 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 919 168 moveto
-929 164 lineto
-919 161 lineto
-closepath
-stroke
-end grestore
-
-% Indrec
-gsave 10 dict begin
-251 271 31 18 ellipse_path
-stroke
-gsave 10 dict begin
-233 266 moveto
-(Indrec)
-[4.56 6.96 6.96 4.56 6.24 6.24]
-xshow
-end grestore
-end grestore
-
-% Pretyping -> Indrec
-newpath 69 195 moveto
-83 202 101 209 116 216 curveto
-150 230 188 246 216 257 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 214 260 moveto
-225 261 lineto
-217 254 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 214 260 moveto
-225 261 lineto
-217 254 lineto
-closepath
-stroke
-end grestore
-
-% Coercion
-gsave 10 dict begin
-251 67 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-225 62 moveto
-(Coercion)
-[9.36 6.96 6.24 4.56 6.24 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Cases -> Coercion
-newpath 176 65 moveto
-184 65 193 66 202 66 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 202 70 moveto
-212 66 lineto
-202 63 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 202 70 moveto
-212 66 lineto
-202 63 lineto
-closepath
-stroke
-end grestore
-
-% Detyping -> Inductiveops
-newpath 1009 164 moveto
-1022 164 1036 164 1050 164 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1050 168 moveto
-1060 164 lineto
-1050 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1050 168 moveto
-1060 164 lineto
-1050 161 lineto
-closepath
-stroke
-end grestore
-
-% Detyping -> Rawterm
-newpath 999 152 moveto
-1020 144 1047 133 1069 125 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1070 128 moveto
-1079 122 lineto
-1068 122 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1070 128 moveto
-1079 122 lineto
-1068 122 lineto
-closepath
-stroke
-end grestore
-
-% Indrec -> Inductiveops
-newpath 281 276 moveto
-325 283 412 294 485 294 curveto
-485 294 485 294 839 294 curveto
-937 294 1036 225 1082 188 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1085 190 moveto
-1090 181 lineto
-1080 185 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1085 190 moveto
-1090 181 lineto
-1080 185 lineto
-closepath
-stroke
-end grestore
-
-% Matching
-gsave 10 dict begin
-610 248 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-582 243 moveto
-(Matching)
-[12.48 6.24 3.84 6 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Matching -> Pattern
-newpath 643 237 moveto
-658 232 675 227 689 222 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 690 225 moveto
-699 219 lineto
-688 219 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 690 225 moveto
-699 219 lineto
-688 219 lineto
-closepath
-stroke
-end grestore
-
-% Matching -> Reductionops
-newpath 650 250 moveto
-696 253 773 256 839 256 curveto
-839 256 839 256 969 256 curveto
-1059 256 1159 212 1210 184 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1212 187 moveto
-1219 179 lineto
-1209 181 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1212 187 moveto
-1219 179 lineto
-1209 181 lineto
-closepath
-stroke
-end grestore
-
-% Evarconv
-gsave 10 dict begin
-366 67 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-339 62 moveto
-(Evarconv)
-[8.4 6.72 6.24 4.56 6.24 6.96 6.48 6.96]
-xshow
-end grestore
-end grestore
-
-% Evarconv -> Evarutil
-newpath 406 68 moveto
-474 69 610 71 682 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 682 76 moveto
-692 72 lineto
-682 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 682 76 moveto
-692 72 lineto
-682 69 lineto
-closepath
-stroke
-end grestore
-
-% Evarconv -> Recordops
-newpath 397 56 moveto
-411 51 428 45 442 39 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 443 42 moveto
-452 36 lineto
-441 36 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 443 42 moveto
-452 36 lineto
-441 36 lineto
-closepath
-stroke
-end grestore
-
-% Coercion -> Evarconv
-newpath 290 67 moveto
-299 67 307 67 316 67 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 316 71 moveto
-326 67 lineto
-316 64 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 316 71 moveto
-326 67 lineto
-316 64 lineto
-closepath
-stroke
-end grestore
-
-% Clenv
-gsave 10 dict begin
-146 118 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-129 113 moveto
-(Clenv)
-[9.36 3.84 6.24 6.48 6.96]
-xshow
-end grestore
-end grestore
-
-% Clenv -> Unification
-newpath 176 118 moveto
-252 118 455 118 554 118 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 554 122 moveto
-564 118 lineto
-554 115 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 554 122 moveto
-564 118 lineto
-554 115 lineto
-closepath
-stroke
-end grestore
-
-% Clenv -> Coercion
-newpath 170 107 moveto
-183 100 200 93 215 85 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 217 88 moveto
-224 80 lineto
-214 82 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 217 88 moveto
-224 80 lineto
-214 82 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps
deleted file mode 100644
index 4dd045ce..00000000
--- a/dev/ocamlweb-doc/proofs.dep.ps
+++ /dev/null
@@ -1,649 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007)
-%%For: (notin) Jean-Marc Notin,,,
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: (atend)
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-EncodingVector 45 /hyphen put
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-setupLatin1
-%%Page: 1 1
-%%PageBoundingBox: 36 36 576 753
-%%PageOrientation: Landscape
-gsave
-36 36 576 753 boxprim clip newpath
-0 0 1 beginpage
-0.870968 0.870968 set_scale 90 rotate 45.3333 -657.333 translate
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 616 lineto
-819 616 lineto
-819 -4 lineto
-closepath fill
-0.870968 setlinewidth
-0.000 0.000 1.000 graphcolor
-newpath -4 -4 moveto
--4 616 lineto
-819 616 lineto
-819 -4 lineto
-closepath stroke
-% Clenvtac
-gsave
-0.502 1.000 0.820 nodecolor
-451 522 37.1753 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-451 522 37.1753 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-451 517 moveto 49 -0.5 (Clenvtac) alignedtext
-grestore
-% Evar_refiner
-gsave
-0.502 1.000 0.820 nodecolor
-439 450 49.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 450 49.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 445 moveto 72 -0.5 (Evar_refiner) alignedtext
-grestore
-% Clenvtac->Evar_refiner
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 448 504 moveto
-447 496 445 487 444 478 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 447.393 477.119 moveto
-442 468 lineto
-440.529 478.492 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 447.393 477.119 moveto
-442 468 lineto
-440.529 478.492 lineto
-closepath stroke
-grestore
-% Tacmach
-gsave
-0.502 1.000 0.820 nodecolor
-711 450 38.1754 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-711 450 38.1754 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-711 445 moveto 51 -0.5 (Tacmach) alignedtext
-grestore
-% Clenvtac->Tacmach
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 483 513 moveto
-530 500 616 476 668 462 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 669.427 465.226 moveto
-678 459 lineto
-667.416 458.521 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 669.427 465.226 moveto
-678 459 lineto
-667.416 458.521 lineto
-closepath stroke
-grestore
-% Refiner
-gsave
-0.502 1.000 0.820 nodecolor
-439 378 34.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 378 34.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 373 moveto 42 -0.5 (Refiner) alignedtext
-grestore
-% Evar_refiner->Refiner
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 439 432 moveto
-439 424 439 415 439 406 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 442.5 406 moveto
-439 396 lineto
-435.5 406 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 442.5 406 moveto
-439 396 lineto
-435.5 406 lineto
-closepath stroke
-grestore
-% Tacmach->Refiner
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 678 441 moveto
-628 428 533 403 480 389 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 480.584 385.521 moveto
-470 386 lineto
-478.573 392.226 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 480.584 385.521 moveto
-470 386 lineto
-478.573 392.226 lineto
-closepath stroke
-grestore
-% Redexpr
-gsave
-0.502 1.000 0.820 nodecolor
-711 378 36.1752 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-711 378 36.1752 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-711 373 moveto 47 -0.5 (Redexpr) alignedtext
-grestore
-% Tacmach->Redexpr
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 711 432 moveto
-711 424 711 415 711 406 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 714.5 406 moveto
-711 396 lineto
-707.5 406 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 714.5 406 moveto
-711 396 lineto
-707.5 406 lineto
-closepath stroke
-grestore
-% Decl_mode
-gsave
-0.502 1.000 0.820 nodecolor
-698 594 45.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-698 594 45.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-698 589 moveto 64 -0.5 (Decl_mode) alignedtext
-grestore
-% Pfedit
-gsave
-0.502 1.000 0.820 nodecolor
-698 522 30.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-698 522 30.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-698 517 moveto 34 -0.5 (Pfedit) alignedtext
-grestore
-% Decl_mode->Pfedit
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 698 576 moveto
-698 568 698 559 698 550 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 701.5 550 moveto
-698 540 lineto
-694.5 550 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 701.5 550 moveto
-698 540 lineto
-694.5 550 lineto
-closepath stroke
-grestore
-% Pfedit->Evar_refiner
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 671 514 moveto
-628 503 543 479 488 464 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 488.584 460.521 moveto
-478 461 lineto
-486.573 467.226 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 488.584 460.521 moveto
-478 461 lineto
-486.573 467.226 lineto
-closepath stroke
-grestore
-% Pfedit->Tacmach
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 701 504 moveto
-702 496 704 487 706 478 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 709.471 478.492 moveto
-708 468 lineto
-702.607 477.119 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 709.471 478.492 moveto
-708 468 lineto
-702.607 477.119 lineto
-closepath stroke
-grestore
-% Logic
-gsave
-0.502 1.000 0.820 nodecolor
-439 306 29.1747 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 306 29.1747 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 301 moveto 33 -0.5 (Logic) alignedtext
-grestore
-% Refiner->Logic
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 439 360 moveto
-439 352 439 343 439 334 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 442.5 334 moveto
-439 324 lineto
-435.5 334 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 442.5 334 moveto
-439 324 lineto
-435.5 334 lineto
-closepath stroke
-grestore
-% Proof_trees
-gsave
-0.502 1.000 0.820 nodecolor
-439 234 45.1757 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 234 45.1757 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 229 moveto 65 -0.5 (Proof_trees) alignedtext
-grestore
-% Logic->Proof_trees
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 439 288 moveto
-439 280 439 271 439 262 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 442.5 262 moveto
-439 252 lineto
-435.5 262 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 442.5 262 moveto
-439 252 lineto
-435.5 262 lineto
-closepath stroke
-grestore
-% Proof_type
-gsave
-0.502 1.000 0.820 nodecolor
-439 162 44.1757 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 162 44.1757 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 157 moveto 63 -0.5 (Proof_type) alignedtext
-grestore
-% Proof_trees->Proof_type
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 439 216 moveto
-439 208 439 199 439 190 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 442.5 190 moveto
-439 180 lineto
-435.5 190 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 442.5 190 moveto
-439 180 lineto
-435.5 190 lineto
-closepath stroke
-grestore
-% Decl_expr
-gsave
-0.502 1.000 0.820 nodecolor
-439 90 42.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 90 42.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 85 moveto 58 -0.5 (Decl_expr) alignedtext
-grestore
-% Proof_type->Decl_expr
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 439 144 moveto
-439 136 439 127 439 118 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 442.5 118 moveto
-439 108 lineto
-435.5 118 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 442.5 118 moveto
-439 108 lineto
-435.5 118 lineto
-closepath stroke
-grestore
-% Tacexpr
-gsave
-0.502 1.000 0.820 nodecolor
-439 18 36.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-439 18 36.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-439 13 moveto 46 -0.5 (Tacexpr) alignedtext
-grestore
-% Decl_expr->Tacexpr
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 439 72 moveto
-439 64 439 55 439 46 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 442.5 46 moveto
-439 36 lineto
-435.5 46 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 442.5 46 moveto
-439 36 lineto
-435.5 46 lineto
-closepath stroke
-grestore
-% Tactic_debug
-gsave
-0.502 1.000 0.820 nodecolor
-133 450 51.1777 18 ellipse_path fill
-0.870968 setlinewidth
-filled
-0.502 1.000 0.820 nodecolor
-133 450 51.1777 18 ellipse_path stroke
-0.000 0.000 0.000 nodecolor
-14.00 /Times-Roman set_font
-133 445 moveto 76 -0.5 (Tactic_debug) alignedtext
-grestore
-% Tactic_debug->Refiner
-gsave
-0.870968 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 176 440 moveto
-234 426 339 401 398 387 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 398.881 390.393 moveto
-408 385 lineto
-397.508 383.529 lineto
-closepath fill
-0.870968 setlinewidth
-solid
-0.000 0.000 0.000 edgecolor
-newpath 398.881 390.393 moveto
-408 385 lineto
-397.508 383.529 lineto
-closepath stroke
-grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-%%BoundingBox: 36 36 576 753
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly
deleted file mode 100644
index bfc7d5cc..00000000
--- a/dev/ocamlweb-doc/syntax.mly
+++ /dev/null
@@ -1,224 +0,0 @@
-%{
-open Ast
-open Parse
-%}
-
-%token <string> META INT IDENT
-%token <string> OPER
-%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF
-%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX
-%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT
-%token EOF
-
-%start main
-%type <Ast.constr_ast> main
-
-%start constr
-%type <Ast.constr_ast> constr
-
-%start simple_constr
-%type <Ast.constr_ast> simple_constr
-
-%%
-
-main:
- constr EOF { $1 }
-;
-
-
-paren_constr:
- constr COMMA paren_constr { Pair($1,$3) }
- | constr { $1 }
-;
-
-constr:
- binder_constr { $1 }
- | oper_constr { close_stack $1 }
-;
-
-binder_constr:
- BANG ne_binders DOT constr { Prod($2, $4) }
- | FUN ne_binders type_cstr RARROW constr { Lambda($2,mk_cast $5 $3) }
- | LET IDENT binders type_cstr COLONEQ constr IN constr
- { Let($2,mk_lambda $3 (mk_cast $6 $4),$8) }
- | LET LPAR comma_binders RPAR COLONEQ constr IN constr
- { LetCase($3,$6,$8) }
- | IF constr THEN constr ELSE constr { IfCase($2,$4,$6) }
- | fix_constr { $1 }
- | EVAL rfun IN constr { Eval($2,$4) }
-;
-
-comma_binders:
- ne_comma_binders { $1 }
- | { [] }
-;
-
-ne_comma_binders:
- binder COMMA ne_comma_binders { $1 :: $3 }
- | binder { [$1] }
-;
-
-rfun:
- SIMPL { Simpl }
-;
-
-
-/* 2 Conflits shift/reduce */
-oper_constr:
- oper_constr oper appl_constr
- { parse_term $3 (parse_oper $2 $1) }
- | oper_constr oper binder_constr
- { parse_term $3 (parse_oper $2 $1) }
- | oper_constr oper { parse_oper $2 $1 }
- | { empty }
- | appl_constr { parse_term $1 empty }
-;
-
-oper:
- OPER {$1}
- | COLON {":"}
-;
-
-appl_constr:
- simple_constr ne_appl_args { Appl($1,$2) }
- | AT global simple_constrs { ApplExpl($2,$3) }
- | simple_constr { $1 }
-;
-
-appl_arg:
- AT INT COLONEQ simple_constr { (Some $2,$4) }
- | simple_constr { (None,$1) }
-;
-
-ne_appl_args:
- appl_arg { [$1] }
- | appl_arg ne_appl_args { $1::$2 }
-;
-
-simple_constr:
- atomic_constr { $1 }
- | match_constr { $1 }
- | LPAR paren_constr RPAR { $2 }
- | simple_constr PERCENT IDENT { Scope($3,$1) }
-;
-
-simple_constrs:
- simple_constr simple_constrs { $1::$2 }
- | { [] }
-;
-
-atomic_constr:
- global { Qualid $1 }
- | PROP { Prop }
- | SET { Set }
- | TYPE { Type }
- | INT { Int $1 }
- | WILDCARD { Hole }
- | META { Meta $1 }
-;
-
-global:
- IDENT DOT global { $1 :: $3 }
- | IDENT { [$1] }
-;
-
-/* Conflit normal */
-fix_constr:
- fix_kw fix_decl
- { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) }
- | fix_kw fix_decl fix_decls FOR IDENT { Fixp($1, $2::$3, $5) }
-;
-
-fix_kw: FIX {Fix} | COFIX {CoFix}
-;
-
-fix_decl:
- IDENT binders type_cstr annot COLONEQ constr { ($1,$2,$3,$4,$6) }
-;
-
-fix_decls:
- AND fix_decl fix_decls { $2::$3 }
- | AND fix_decl { [$2] }
-;
-
-annot:
- LBRACE STRUCT IDENT RBRACE { Some $3 }
- | { None }
-;
-
-match_constr:
- MATCH case_items case_type WITH branches END { Match($2,$3,$5) }
-;
-
-case_items:
- case_item { [$1] }
- | case_item COMMA case_items { $1::$3 }
-;
-
-case_item:
- constr pred_pattern { ($1,$2) }
-;
-
-case_type:
- RARROW constr { Some $2 }
- | { None }
-;
-
-pred_pattern:
- AS IDENT COLON constr { (Some $2, Some $4) }
- | AS IDENT { (Some $2, None) }
- | COLON constr { (None, Some $2) }
- | { (None,None) }
-;
-
-branches:
- BAR branch_list { $2 }
- | branch_list { $1 }
- | { [] }
-;
-
-branch_list:
- patterns RARROW constr { [$1, $3] }
- | patterns RARROW constr BAR branch_list { ($1,$3)::$5 }
-;
-
-patterns:
- pattern { [$1] }
- | pattern COMMA patterns { $1::$3 }
-;
-
-pattern:
- pattern AS IDENT { PatAs($1,$3) }
- | pattern COLON constr { PatType($1,$3) }
- | IDENT simple_patterns { PatConstr($1,$2) }
- | simple_pattern { $1 }
-;
-
-simple_pattern:
- IDENT { PatVar $1 }
- | LPAR pattern RPAR { $2 }
-;
-
-simple_patterns:
- simple_pattern { [$1] }
- | simple_pattern simple_patterns { $1::$2 }
-;
-
-binder:
- IDENT { ($1,Hole) }
- | LPAR IDENT type_cstr RPAR { ($2,$3) }
-;
-
-binders:
- ne_binders { $1 }
- | { [] }
-
-ne_binders:
- binder { [$1] }
- | binder ne_binders { $1::$2 }
-;
-
-type_cstr:
- COLON constr { $2 }
- | { Hole }
-;
diff --git a/dev/ocamlweb-doc/tactics.dep.ps b/dev/ocamlweb-doc/tactics.dep.ps
deleted file mode 100644
index f4de22b7..00000000
--- a/dev/ocamlweb-doc/tactics.dep.ps
+++ /dev/null
@@ -1,991 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: 35 35 577 165
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
- dup 306 /AE
- dup 301 /Aacute
- dup 302 /Acircumflex
- dup 304 /Adieresis
- dup 300 /Agrave
- dup 305 /Aring
- dup 303 /Atilde
- dup 307 /Ccedilla
- dup 311 /Eacute
- dup 312 /Ecircumflex
- dup 313 /Edieresis
- dup 310 /Egrave
- dup 315 /Iacute
- dup 316 /Icircumflex
- dup 317 /Idieresis
- dup 314 /Igrave
- dup 334 /Udieresis
- dup 335 /Yacute
- dup 376 /thorn
- dup 337 /germandbls
- dup 341 /aacute
- dup 342 /acircumflex
- dup 344 /adieresis
- dup 346 /ae
- dup 340 /agrave
- dup 345 /aring
- dup 347 /ccedilla
- dup 351 /eacute
- dup 352 /ecircumflex
- dup 353 /edieresis
- dup 350 /egrave
- dup 355 /iacute
- dup 356 /icircumflex
- dup 357 /idieresis
- dup 354 /igrave
- dup 360 /dcroat
- dup 361 /ntilde
- dup 363 /oacute
- dup 364 /ocircumflex
- dup 366 /odieresis
- dup 362 /ograve
- dup 365 /otilde
- dup 370 /oslash
- dup 372 /uacute
- dup 373 /ucircumflex
- dup 374 /udieresis
- dup 371 /ugrave
- dup 375 /yacute
- dup 377 /ydieresis
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- dup scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-%%Page: 1 1
-%%PageBoundingBox: 36 36 577 165
-%%PageOrientation: Portrait
-gsave
-35 35 542 130 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0.4696 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-% Extraargs
-gsave 10 dict begin
-483 110 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-455 105 moveto
-(Extraargs)
-[8.4 6.96 3.84 4.56 6.24 6.24 4.32 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-% Setoid_replace
-gsave 10 dict begin
-615 64 54 18 ellipse_path
-stroke
-gsave 10 dict begin
-573 59 moveto
-(Setoid_replace)
-[7.68 6 3.84 6.96 3.84 6.96 6.96 4.56 6.24 6.96 3.84 6.24 6.24 6.24]
-xshow
-end grestore
-end grestore
-
-% Extraargs -> Setoid_replace
-newpath 515 99 moveto
-531 93 550 87 567 81 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 569 84 moveto
-577 77 lineto
-566 77 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 569 84 moveto
-577 77 lineto
-566 77 lineto
-closepath
-stroke
-end grestore
-
-% Tactics
-gsave 10 dict begin
-884 110 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-864 105 moveto
-(Tactics)
-[7.44 6.24 6.24 3.84 3.84 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-% Setoid_replace -> Tactics
-newpath 669 66 moveto
-709 68 764 72 810 83 curveto
-823 85 837 90 848 94 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 847 98 moveto
-858 98 lineto
-850 91 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 847 98 moveto
-858 98 lineto
-850 91 lineto
-closepath
-stroke
-end grestore
-
-% Termdn
-gsave 10 dict begin
-998 256 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-976 251 moveto
-(Termdn)
-[7.2 6.24 4.8 10.8 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Dn
-gsave 10 dict begin
-1112 256 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-1102 251 moveto
-(Dn)
-[10.08 6.96]
-xshow
-end grestore
-end grestore
-
-% Termdn -> Dn
-newpath 1033 256 moveto
-1047 256 1061 256 1075 256 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1075 260 moveto
-1085 256 lineto
-1075 253 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1075 260 moveto
-1085 256 lineto
-1075 253 lineto
-closepath
-stroke
-end grestore
-
-% Hipattern
-gsave 10 dict begin
-998 110 40 18 ellipse_path
-stroke
-gsave 10 dict begin
-971 105 moveto
-(Hipattern)
-[10.08 3.84 6.96 6.24 3.84 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-% Tactics -> Hipattern
-newpath 917 110 moveto
-927 110 938 110 948 110 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 948 114 moveto
-958 110 lineto
-948 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 948 114 moveto
-958 110 lineto
-948 107 lineto
-closepath
-stroke
-end grestore
-
-% Tacticals
-gsave 10 dict begin
-1112 110 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-1087 105 moveto
-(Tacticals)
-[7.44 6.24 6.24 3.84 3.84 6.24 6.24 3.84 5.52]
-xshow
-end grestore
-end grestore
-
-% Hipattern -> Tacticals
-newpath 1038 110 moveto
-1047 110 1055 110 1064 110 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1064 114 moveto
-1074 110 lineto
-1064 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1064 114 moveto
-1074 110 lineto
-1064 107 lineto
-closepath
-stroke
-end grestore
-
-% Tacinterp
-gsave 10 dict begin
-170 191 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-143 186 moveto
-(Tacinterp)
-[7.44 6.24 6.24 3.84 6.96 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-% Auto
-gsave 10 dict begin
-483 218 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-468 213 moveto
-(Auto)
-[9.6 6.96 3.84 6.96]
-xshow
-end grestore
-end grestore
-
-% Tacinterp -> Auto
-newpath 209 194 moveto
-269 200 386 210 445 215 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 445 218 moveto
-455 216 lineto
-445 212 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 445 218 moveto
-455 216 lineto
-445 212 lineto
-closepath
-stroke
-end grestore
-
-% Leminv
-gsave 10 dict begin
-281 166 35 18 ellipse_path
-stroke
-gsave 10 dict begin
-259 161 moveto
-(Leminv)
-[8.4 6.24 10.8 3.84 6.48 6.96]
-xshow
-end grestore
-end grestore
-
-% Tacinterp -> Leminv
-newpath 205 183 moveto
-216 181 228 178 239 175 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 240 178 moveto
-249 173 lineto
-239 172 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 240 178 moveto
-249 173 lineto
-239 172 lineto
-closepath
-stroke
-end grestore
-
-% Hiddentac
-gsave 10 dict begin
-615 164 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-585 159 moveto
-(Hiddentac)
-[10.08 3.84 6.96 6.96 6.24 6.96 4.08 6.24 6.24]
-xshow
-end grestore
-end grestore
-
-% Auto -> Hiddentac
-newpath 507 208 moveto
-526 200 553 189 574 181 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 576 184 moveto
-584 177 lineto
-573 177 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 576 184 moveto
-584 177 lineto
-573 177 lineto
-closepath
-stroke
-end grestore
-
-% Dhyp
-gsave 10 dict begin
-615 218 29 18 ellipse_path
-stroke
-gsave 10 dict begin
-599 213 moveto
-(Dhyp)
-[10.08 6.48 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Auto -> Dhyp
-newpath 511 218 moveto
-530 218 555 218 576 218 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 576 222 moveto
-586 218 lineto
-576 215 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 576 222 moveto
-586 218 lineto
-576 215 lineto
-closepath
-stroke
-end grestore
-
-% Inv
-gsave 10 dict begin
-379 164 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-369 159 moveto
-(Inv)
-[4.56 6.48 6.96]
-xshow
-end grestore
-end grestore
-
-% Leminv -> Inv
-newpath 316 165 moveto
-324 165 333 165 342 165 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 342 169 moveto
-352 165 lineto
-342 162 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 342 169 moveto
-352 165 lineto
-342 162 lineto
-closepath
-stroke
-end grestore
-
-% Refine
-gsave 10 dict begin
-758 110 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-739 105 moveto
-(Refine)
-[9.12 6.24 4.8 3.84 6.96 6.24]
-xshow
-end grestore
-end grestore
-
-% Refine -> Tactics
-newpath 790 110 moveto
-805 110 824 110 841 110 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 841 114 moveto
-851 110 lineto
-841 107 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 841 114 moveto
-851 110 lineto
-841 107 lineto
-closepath
-stroke
-end grestore
-
-% Nbtermdn
-gsave 10 dict begin
-758 256 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-729 251 moveto
-(Nbtermdn)
-[10.08 6.96 3.84 6.24 4.8 10.8 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Btermdn
-gsave 10 dict begin
-884 256 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-859 251 moveto
-(Btermdn)
-[9.36 3.84 6.24 4.8 10.8 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Nbtermdn -> Btermdn
-newpath 800 256 moveto
-812 256 824 256 836 256 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 836 260 moveto
-846 256 lineto
-836 253 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 836 260 moveto
-846 256 lineto
-836 253 lineto
-closepath
-stroke
-end grestore
-
-% Btermdn -> Termdn
-newpath 922 256 moveto
-932 256 943 256 953 256 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 953 260 moveto
-963 256 lineto
-953 253 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 953 260 moveto
-963 256 lineto
-953 253 lineto
-closepath
-stroke
-end grestore
-
-% Elim
-gsave 10 dict begin
-483 164 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-468 159 moveto
-(Elim)
-[8.4 3.84 3.84 10.8]
-xshow
-end grestore
-end grestore
-
-% Inv -> Elim
-newpath 406 164 moveto
-418 164 432 164 445 164 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 445 168 moveto
-455 164 lineto
-445 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 445 168 moveto
-455 164 lineto
-445 161 lineto
-closepath
-stroke
-end grestore
-
-% Equality
-gsave 10 dict begin
-483 56 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-459 51 moveto
-(Equality)
-[8.4 6.72 6.96 6.24 3.84 3.84 3.84 6.96]
-xshow
-end grestore
-end grestore
-
-% Inv -> Equality
-newpath 390 147 moveto
-401 130 421 102 442 83 curveto
-445 80 448 78 451 76 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 453 79 moveto
-459 70 lineto
-449 73 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 453 79 moveto
-459 70 lineto
-449 73 lineto
-closepath
-stroke
-end grestore
-
-% Elim -> Hiddentac
-newpath 511 164 moveto
-526 164 545 164 562 164 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 562 168 moveto
-572 164 lineto
-562 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 562 168 moveto
-572 164 lineto
-562 161 lineto
-closepath
-stroke
-end grestore
-
-% Equality -> Setoid_replace
-newpath 520 58 moveto
-530 59 540 60 551 60 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 551 63 moveto
-561 61 lineto
-551 57 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 551 63 moveto
-561 61 lineto
-551 57 lineto
-closepath
-stroke
-end grestore
-
-% Evar_tactics
-gsave 10 dict begin
-758 164 48 18 ellipse_path
-stroke
-gsave 10 dict begin
-722 159 moveto
-(Evar_tactics)
-[8.4 6.72 6.24 4.56 6.96 4.08 6.24 6.24 3.84 3.84 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-% Hiddentac -> Evar_tactics
-newpath 658 164 moveto
-671 164 685 164 699 164 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 699 168 moveto
-709 164 lineto
-699 161 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 699 168 moveto
-709 164 lineto
-699 161 lineto
-closepath
-stroke
-end grestore
-
-% Evar_tactics -> Tactics
-newpath 790 150 moveto
-808 142 830 132 849 125 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 850 128 moveto
-858 121 lineto
-847 122 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 850 128 moveto
-858 121 lineto
-847 122 lineto
-closepath
-stroke
-end grestore
-
-% Dhyp -> Tactics
-newpath 644 219 moveto
-684 220 756 217 810 191 curveto
-844 175 855 163 872 137 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 875 138 moveto
-877 128 lineto
-869 135 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 875 138 moveto
-877 128 lineto
-869 135 lineto
-closepath
-stroke
-end grestore
-
-% Dhyp -> Nbtermdn
-newpath 642 225 moveto
-662 230 689 238 712 244 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 712 247 moveto
-722 246 lineto
-713 241 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 712 247 moveto
-722 246 lineto
-713 241 lineto
-closepath
-stroke
-end grestore
-
-% Contradiction
-gsave 10 dict begin
-758 18 51 18 ellipse_path
-stroke
-gsave 10 dict begin
-719 13 moveto
-(Contradiction)
-[9.36 6.96 6.96 3.84 4.56 6.24 6.96 3.84 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Contradiction -> Tactics
-newpath 784 34 moveto
-793 39 802 44 810 50 curveto
-827 62 845 76 859 88 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 857 91 moveto
-867 95 lineto
-862 86 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 857 91 moveto
-867 95 lineto
-862 86 lineto
-closepath
-stroke
-end grestore
-
-% Autorewrite
-gsave 10 dict begin
-47 191 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 186 moveto
-(Autorewrite)
-[9.6 6.96 3.84 6.96 4.56 5.76 10.08 4.8 3.84 3.84 6.24]
-xshow
-end grestore
-end grestore
-
-% Autorewrite -> Tacinterp
-newpath 94 191 moveto
-102 191 111 191 120 191 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 120 195 moveto
-130 191 lineto
-120 188 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 120 195 moveto
-130 191 lineto
-120 188 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF
diff --git a/dev/ocamlweb-doc/toplevel.dep.ps b/dev/ocamlweb-doc/toplevel.dep.ps
deleted file mode 100644
index e0355aac..00000000
--- a/dev/ocamlweb-doc/toplevel.dep.ps
+++ /dev/null
@@ -1,971 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
-%%For: (herbelin) Hugo Herbelin
-%%Title: G
-%%Pages: (atend)
-%%BoundingBox: 35 35 577 166
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
- dup 306 /AE
- dup 301 /Aacute
- dup 302 /Acircumflex
- dup 304 /Adieresis
- dup 300 /Agrave
- dup 305 /Aring
- dup 303 /Atilde
- dup 307 /Ccedilla
- dup 311 /Eacute
- dup 312 /Ecircumflex
- dup 313 /Edieresis
- dup 310 /Egrave
- dup 315 /Iacute
- dup 316 /Icircumflex
- dup 317 /Idieresis
- dup 314 /Igrave
- dup 334 /Udieresis
- dup 335 /Yacute
- dup 376 /thorn
- dup 337 /germandbls
- dup 341 /aacute
- dup 342 /acircumflex
- dup 344 /adieresis
- dup 346 /ae
- dup 340 /agrave
- dup 345 /aring
- dup 347 /ccedilla
- dup 351 /eacute
- dup 352 /ecircumflex
- dup 353 /edieresis
- dup 350 /egrave
- dup 355 /iacute
- dup 356 /icircumflex
- dup 357 /idieresis
- dup 354 /igrave
- dup 360 /dcroat
- dup 361 /ntilde
- dup 363 /oacute
- dup 364 /ocircumflex
- dup 366 /odieresis
- dup 362 /ograve
- dup 365 /otilde
- dup 370 /oslash
- dup 372 /uacute
- dup 373 /ucircumflex
- dup 374 /udieresis
- dup 371 /ugrave
- dup 375 /yacute
- dup 377 /ydieresis
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
- dup dup findfont dup length dict begin
- { 1 index /FID ne { def }{ pop pop } ifelse
- } forall
- /Encoding EncodingVector def
- currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
- dup 1 exch div /InvScaleFactor exch def
- dup scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage { % i j npages
- /npages exch def
- /j exch def
- /i exch def
- /str 10 string def
- npages 1 gt {
- gsave
- coordfont setfont
- 0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
- grestore
- } if
-} bind def
-
-/set_font {
- findfont exch
- scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext { % width adj text
- /text exch def
- /adj exch def
- /width exch def
- gsave
- width 0 gt {
- text stringwidth pop adj mul 0 rmoveto
- } if
- [] 0 setdash
- text show
- grestore
-} def
-
-/boxprim { % xcorner ycorner xsize ysize
- 4 2 roll
- moveto
- 2 copy
- exch 0 rlineto
- 0 exch rlineto
- pop neg 0 rlineto
- closepath
-} bind def
-
-/ellipse_path {
- /ry exch def
- /rx exch def
- /y exch def
- /x exch def
- matrix currentmatrix
- newpath
- x y translate
- rx ry scale
- 0 0 1 0 360 arc
- setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
- [ % layer color sequence - darkest to lightest
- [0 0 0]
- [.2 .8 .8]
- [.4 .8 .8]
- [.6 .8 .8]
- [.8 .8 .8]
- ]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer 1 sub layerlen mod get
- aload pop sethsbcolor
- /nodecolor {nopcolor} def
- /edgecolor {nopcolor} def
- /graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
- /myupper exch def
- /mylower exch def
- curlayer mylower lt
- curlayer myupper gt
- or
- {invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
- userdict (<<) cvn ([) cvn load put
- userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-%%Page: 1 1
-%%PageBoundingBox: 36 36 577 166
-%%PageOrientation: Portrait
-gsave
-35 35 542 131 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0.4180 set_scale
-0 0 translate 0 rotate
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-% Vernac
-gsave 10 dict begin
-562 145 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-541 140 moveto
-(Vernac)
-[8.88 6.24 4.8 6.96 6.24 6.24]
-xshow
-end grestore
-end grestore
-
-% Vernacentries
-gsave 10 dict begin
-724 158 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-685 153 moveto
-(Vernacentries)
-[8.88 6.24 4.8 6.96 6.24 6.24 6.24 6.96 3.84 4.8 3.84 6.24 5.52]
-xshow
-end grestore
-end grestore
-
-% Vernac -> Vernacentries
-newpath 595 148 moveto
-615 149 640 151 663 153 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 663 156 moveto
-673 154 lineto
-663 150 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 663 156 moveto
-673 154 lineto
-663 150 lineto
-closepath
-stroke
-end grestore
-
-% Vernacinterp
-gsave 10 dict begin
-862 158 50 18 ellipse_path
-stroke
-gsave 10 dict begin
-825 153 moveto
-(Vernacinterp)
-[8.88 6.24 4.8 6.96 6.24 6.24 3.84 6.96 3.84 6.24 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-% Vernacentries -> Vernacinterp
-newpath 776 158 moveto
-785 158 793 158 802 158 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 802 162 moveto
-812 158 lineto
-802 155 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 802 162 moveto
-812 158 lineto
-802 155 lineto
-closepath
-stroke
-end grestore
-
-% Discharge
-gsave 10 dict begin
-862 212 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-833 207 moveto
-(Discharge)
-[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24]
-xshow
-end grestore
-end grestore
-
-% Vernacentries -> Discharge
-newpath 758 171 moveto
-777 179 801 188 822 196 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 820 199 moveto
-831 200 lineto
-823 193 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 820 199 moveto
-831 200 lineto
-823 193 lineto
-closepath
-stroke
-end grestore
-
-% Mltop
-gsave 10 dict begin
-862 104 31 18 ellipse_path
-stroke
-gsave 10 dict begin
-844 99 moveto
-(Mltop)
-[12.48 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Vernacentries -> Mltop
-newpath 758 145 moveto
-779 137 805 126 826 118 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 828 121 moveto
-836 114 lineto
-825 114 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 828 121 moveto
-836 114 lineto
-825 114 lineto
-closepath
-stroke
-end grestore
-
-% Record
-gsave 10 dict begin
-862 281 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-842 276 moveto
-(Record)
-[9.12 6.24 6.24 6.96 4.32 6.96]
-xshow
-end grestore
-end grestore
-
-% Vernacentries -> Record
-newpath 742 175 moveto
-760 192 788 217 812 239 curveto
-819 246 828 253 835 259 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 833 262 moveto
-843 266 lineto
-838 257 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 833 262 moveto
-843 266 lineto
-838 257 lineto
-closepath
-stroke
-end grestore
-
-% Himsg
-gsave 10 dict begin
-991 85 32 18 ellipse_path
-stroke
-gsave 10 dict begin
-971 80 moveto
-(Himsg)
-[10.08 3.84 10.8 5.52 6.96]
-xshow
-end grestore
-end grestore
-
-% Vernacinterp -> Himsg
-newpath 890 143 moveto
-897 139 905 135 912 131 curveto
-929 123 946 112 960 103 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 962 106 moveto
-969 98 lineto
-959 100 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 962 106 moveto
-969 98 lineto
-959 100 lineto
-closepath
-stroke
-end grestore
-
-% Vernacexpr
-gsave 10 dict begin
-1246 221 45 18 ellipse_path
-stroke
-gsave 10 dict begin
-1213 216 moveto
-(Vernacexpr)
-[8.88 6.24 4.8 6.96 6.24 6.24 5.76 6.96 6.96 4.56]
-xshow
-end grestore
-end grestore
-
-% Vernacinterp -> Vernacexpr
-newpath 912 159 moveto
-947 160 994 163 1034 169 curveto
-1092 178 1158 195 1200 207 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1199 210 moveto
-1210 210 lineto
-1201 204 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1199 210 moveto
-1210 210 lineto
-1201 204 lineto
-closepath
-stroke
-end grestore
-
-% Class
-gsave 10 dict begin
-1117 238 28 18 ellipse_path
-stroke
-gsave 10 dict begin
-1101 233 moveto
-(Class)
-[9.36 3.84 6.24 5.52 5.52]
-xshow
-end grestore
-end grestore
-
-% Discharge -> Class
-newpath 902 217 moveto
-917 219 933 221 948 223 curveto
-992 228 1044 232 1079 235 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1079 238 moveto
-1089 236 lineto
-1079 232 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1079 238 moveto
-1089 236 lineto
-1079 232 lineto
-closepath
-stroke
-end grestore
-
-% Recordobj
-gsave 10 dict begin
-991 196 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-962 191 moveto
-(Recordobj)
-[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 3.84]
-xshow
-end grestore
-end grestore
-
-% Discharge -> Recordobj
-newpath 902 207 moveto
-914 205 927 204 940 202 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 940 205 moveto
-950 201 lineto
-940 199 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 940 205 moveto
-950 201 lineto
-940 199 lineto
-closepath
-stroke
-end grestore
-
-% Command
-gsave 10 dict begin
-991 288 42 18 ellipse_path
-stroke
-gsave 10 dict begin
-961 283 moveto
-(Command)
-[9.36 6.96 10.8 10.8 6.24 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Record -> Command
-newpath 895 283 moveto
-908 284 923 285 938 285 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 938 288 moveto
-948 286 lineto
-938 282 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 938 288 moveto
-948 286 lineto
-938 282 lineto
-closepath
-stroke
-end grestore
-
-% Toplevel
-gsave 10 dict begin
-255 72 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-231 67 moveto
-(Toplevel)
-[7.2 6.96 6.96 3.84 5.76 6.48 6.24 3.84]
-xshow
-end grestore
-end grestore
-
-% Protectedtoplevel
-gsave 10 dict begin
-390 72 61 18 ellipse_path
-stroke
-gsave 10 dict begin
-341 67 moveto
-(Protectedtoplevel)
-[7.68 4.56 6.72 3.84 6.24 6.24 3.84 6.24 6.96 3.84 6.96 6.96 3.84 5.76 6.48 6.24 3.84]
-xshow
-end grestore
-end grestore
-
-% Toplevel -> Protectedtoplevel
-newpath 292 72 moveto
-300 72 309 72 318 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 318 76 moveto
-328 72 lineto
-318 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 318 76 moveto
-328 72 lineto
-318 69 lineto
-closepath
-stroke
-end grestore
-
-% Protectedtoplevel -> Vernac
-newpath 425 87 moveto
-455 100 497 117 527 130 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 525 133 moveto
-536 134 lineto
-528 127 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 525 133 moveto
-536 134 lineto
-528 127 lineto
-closepath
-stroke
-end grestore
-
-% Cerrors
-gsave 10 dict begin
-724 65 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-702 60 moveto
-(Cerrors)
-[9.36 6.24 5.04 4.56 6.96 4.56 5.52]
-xshow
-end grestore
-end grestore
-
-% Protectedtoplevel -> Cerrors
-newpath 452 71 moveto
-518 70 621 67 679 66 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 679 70 moveto
-689 66 lineto
-679 63 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 679 70 moveto
-689 66 lineto
-679 63 lineto
-closepath
-stroke
-end grestore
-
-% Line_oriented_parser
-gsave 10 dict begin
-562 26 73 18 ellipse_path
-stroke
-gsave 10 dict begin
-501 21 moveto
-(Line_oriented_parser)
-[8.4 3.84 6.96 6.24 6.96 6.96 4.8 3.84 6.24 6.96 3.84 6.24 6.96 6.96 6.96 6.24 4.56 5.52 6.24 4.56]
-xshow
-end grestore
-end grestore
-
-% Protectedtoplevel -> Line_oriented_parser
-newpath 436 60 moveto
-457 55 481 48 502 42 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 503 45 moveto
-512 39 lineto
-501 39 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 503 45 moveto
-512 39 lineto
-501 39 lineto
-closepath
-stroke
-end grestore
-
-% Metasyntax
-gsave 10 dict begin
-1117 292 46 18 ellipse_path
-stroke
-gsave 10 dict begin
-1083 287 moveto
-(Metasyntax)
-[12.48 6 4.08 6.24 5.52 6.96 6.96 4.08 6.24 6.96]
-xshow
-end grestore
-end grestore
-
-% Command -> Metasyntax
-newpath 1034 289 moveto
-1043 290 1052 290 1061 290 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1061 293 moveto
-1071 291 lineto
-1061 287 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1061 293 moveto
-1071 291 lineto
-1061 287 lineto
-closepath
-stroke
-end grestore
-
-% Command -> Class
-newpath 1022 276 moveto
-1041 268 1065 259 1084 252 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1085 255 moveto
-1093 248 lineto
-1082 249 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1085 255 moveto
-1093 248 lineto
-1082 249 lineto
-closepath
-stroke
-end grestore
-
-% Cerrors -> Himsg
-newpath 758 67 moveto
-796 69 859 73 912 77 curveto
-924 78 937 79 949 80 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 949 83 moveto
-959 81 lineto
-949 77 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 949 83 moveto
-959 81 lineto
-949 77 lineto
-closepath
-stroke
-end grestore
-
-% Minicoq
-gsave 10 dict begin
-38 126 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-13 121 moveto
-(Minicoq)
-[12.48 3.84 6.96 3.84 6.24 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Fhimsg
-gsave 10 dict begin
-147 126 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-125 121 moveto
-(Fhimsg)
-[7.68 6.96 3.84 10.8 5.52 6.96]
-xshow
-end grestore
-end grestore
-
-% Minicoq -> Fhimsg
-newpath 76 126 moveto
-84 126 93 126 102 126 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 102 130 moveto
-112 126 lineto
-102 123 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 102 130 moveto
-112 126 lineto
-102 123 lineto
-closepath
-stroke
-end grestore
-
-% Metasyntax -> Vernacexpr
-newpath 1144 277 moveto
-1163 267 1189 252 1210 241 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 1212 244 moveto
-1219 236 lineto
-1209 238 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 1212 244 moveto
-1219 236 lineto
-1209 238 lineto
-closepath
-stroke
-end grestore
-
-% Coqtop
-gsave 10 dict begin
-38 45 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-17 40 moveto
-(Coqtop)
-[9.36 6.96 6.96 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-% Coqinit
-gsave 10 dict begin
-147 72 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-126 67 moveto
-(Coqinit)
-[9.36 6.96 6.96 3.84 6.96 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-% Coqtop -> Coqinit
-newpath 69 53 moveto
-81 56 94 59 106 62 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 105 65 moveto
-116 65 lineto
-107 59 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 105 65 moveto
-116 65 lineto
-107 59 lineto
-closepath
-stroke
-end grestore
-
-% Usage
-gsave 10 dict begin
-147 18 31 18 ellipse_path
-stroke
-gsave 10 dict begin
-129 13 moveto
-(Usage)
-[10.08 5.52 6.24 6.72 6.24]
-xshow
-end grestore
-end grestore
-
-% Coqtop -> Usage
-newpath 69 37 moveto
-81 34 95 31 108 28 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 109 31 moveto
-118 25 lineto
-107 25 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 109 31 moveto
-118 25 lineto
-107 25 lineto
-closepath
-stroke
-end grestore
-
-% Coqinit -> Toplevel
-newpath 181 72 moveto
-190 72 199 72 208 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 208 76 moveto
-218 72 lineto
-208 69 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 208 76 moveto
-218 72 lineto
-208 69 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 09:32:25 +0000