summaryrefslogtreecommitdiff
path: root/dev/ocamlweb-doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ocamlweb-doc')
-rw-r--r--dev/ocamlweb-doc/Makefile75
-rw-r--r--dev/ocamlweb-doc/ast.ml47
-rw-r--r--dev/ocamlweb-doc/interp.dep.ps583
-rw-r--r--dev/ocamlweb-doc/intro.tex25
-rw-r--r--dev/ocamlweb-doc/kernel.dep.ps1454
-rw-r--r--dev/ocamlweb-doc/lex.mll81
-rw-r--r--dev/ocamlweb-doc/library.dep.ps836
-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.ps638
-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, 8497 insertions, 0 deletions
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile
new file mode 100644
index 00000000..96491017
--- /dev/null
+++ b/dev/ocamlweb-doc/Makefile
@@ -0,0 +1,75 @@
+
+# Makefile for doc/
+
+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: ../%
+ (cd ../$*; ocamldep *.ml *.mli) | ocamldot -lr > $@
+
+%.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
new file mode 100644
index 00000000..2153ef47
--- /dev/null
+++ b/dev/ocamlweb-doc/ast.ml
@@ -0,0 +1,47 @@
+
+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
new file mode 100644
index 00000000..b0554481
--- /dev/null
+++ b/dev/ocamlweb-doc/interp.dep.ps
@@ -0,0 +1,583 @@
+%!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 160
+%%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 160
+%%PageOrientation: Portrait
+gsave
+35 35 542 125 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0.9343 set_scale
+0 0 translate 0 rotate
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+% Syntax_def
+gsave 10 dict begin
+303 110 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+271 105 moveto
+(Syntax_def)
+[7.68 6.96 6.96 4.08 6.24 6.96 6.96 6.96 6.24 4.56]
+xshow
+end grestore
+end grestore
+
+% Notation
+gsave 10 dict begin
+422 60 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+397 55 moveto
+(Notation)
+[9.84 6.72 4.08 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Syntax_def -> Notation
+newpath 334 97 moveto
+350 90 369 83 385 76 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 386 79 moveto
+394 72 lineto
+383 73 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 386 79 moveto
+394 72 lineto
+383 73 lineto
+closepath
+stroke
+end grestore
+
+% Ppextend
+gsave 10 dict begin
+537 60 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+511 55 moveto
+(Ppextend)
+[7.68 6.96 5.76 6.96 3.84 6.24 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Notation -> Ppextend
+newpath 460 60 moveto
+469 60 478 60 488 60 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 488 64 moveto
+498 60 lineto
+488 57 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 488 64 moveto
+498 60 lineto
+488 57 lineto
+closepath
+stroke
+end grestore
+
+% Topconstr
+gsave 10 dict begin
+537 114 41 18 ellipse_path
+stroke
+gsave 10 dict begin
+509 109 moveto
+(Topconstr)
+[7.2 6.96 6.96 6.24 6.96 6.96 5.28 3.84 4.56]
+xshow
+end grestore
+end grestore
+
+% Notation -> Topconstr
+newpath 449 73 moveto
+464 80 483 89 500 97 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 498 100 moveto
+509 101 lineto
+501 94 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 498 100 moveto
+509 101 lineto
+501 94 lineto
+closepath
+stroke
+end grestore
+
+% Modintern
+gsave 10 dict begin
+44 98 43 18 ellipse_path
+stroke
+gsave 10 dict begin
+13 93 moveto
+(Modintern)
+[12.48 6.96 6.96 3.84 6.96 3.84 6.24 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+% Constrintern
+gsave 10 dict begin
+173 98 48 18 ellipse_path
+stroke
+gsave 10 dict begin
+138 93 moveto
+(Constrintern)
+[9.36 6.96 6.96 5.28 3.84 4.8 3.84 6.96 3.84 6.24 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+% Modintern -> Constrintern
+newpath 88 98 moveto
+97 98 106 98 115 98 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 115 102 moveto
+125 98 lineto
+115 95 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 115 102 moveto
+125 98 lineto
+115 95 lineto
+closepath
+stroke
+end grestore
+
+% Constrintern -> Syntax_def
+newpath 220 102 moveto
+229 103 239 104 249 105 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 249 108 moveto
+259 106 lineto
+249 102 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 249 108 moveto
+259 106 lineto
+249 102 lineto
+closepath
+stroke
+end grestore
+
+% Reserve
+gsave 10 dict begin
+303 56 35 18 ellipse_path
+stroke
+gsave 10 dict begin
+280 51 moveto
+(Reserve)
+[9.12 6.24 5.52 6.24 4.8 6.48 6.24]
+xshow
+end grestore
+end grestore
+
+% Constrintern -> Reserve
+newpath 210 86 moveto
+227 81 246 75 263 69 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 264 72 moveto
+273 66 lineto
+262 66 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 264 72 moveto
+273 66 lineto
+262 66 lineto
+closepath
+stroke
+end grestore
+
+% Genarg
+gsave 10 dict begin
+422 114 33 18 ellipse_path
+stroke
+gsave 10 dict begin
+401 109 moveto
+(Genarg)
+[10.08 6.24 6.96 6.24 4.32 6.96]
+xshow
+end grestore
+end grestore
+
+% Genarg -> Topconstr
+newpath 456 114 moveto
+465 114 476 114 486 114 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 486 118 moveto
+496 114 lineto
+486 111 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 486 118 moveto
+496 114 lineto
+486 111 lineto
+closepath
+stroke
+end grestore
+
+% Coqlib
+gsave 10 dict begin
+44 21 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+24 16 moveto
+(Coqlib)
+[9.36 6.96 6.96 3.84 3.84 6.96]
+xshow
+end grestore
+end grestore
+
+% Constrextern
+gsave 10 dict begin
+173 21 49 18 ellipse_path
+stroke
+gsave 10 dict begin
+137 16 moveto
+(Constrextern)
+[9.36 6.96 6.96 5.28 3.84 4.56 5.76 6.96 3.84 6.24 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+% Coqlib -> Constrextern
+newpath 77 21 moveto
+88 21 101 21 114 21 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 114 25 moveto
+124 21 lineto
+114 18 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 114 25 moveto
+124 21 lineto
+114 18 lineto
+closepath
+stroke
+end grestore
+
+% Constrextern -> Notation
+newpath 222 19 moveto
+257 18 307 20 348 29 curveto
+361 31 375 37 388 42 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 386 45 moveto
+397 46 lineto
+389 39 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 386 45 moveto
+397 46 lineto
+389 39 lineto
+closepath
+stroke
+end grestore
+
+% Constrextern -> Reserve
+newpath 213 32 moveto
+228 36 246 41 261 45 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 260 48 moveto
+271 48 lineto
+262 42 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 260 48 moveto
+271 48 lineto
+262 42 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF
diff --git a/dev/ocamlweb-doc/intro.tex b/dev/ocamlweb-doc/intro.tex
new file mode 100644
index 00000000..4cec8673
--- /dev/null
+++ b/dev/ocamlweb-doc/intro.tex
@@ -0,0 +1,25 @@
+
+\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
new file mode 100644
index 00000000..3c00121e
--- /dev/null
+++ b/dev/ocamlweb-doc/kernel.dep.ps
@@ -0,0 +1,1454 @@
+%!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 127
+%%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 127
+%%PageOrientation: Portrait
+gsave
+35 35 542 92 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0.2845 set_scale
+0 0 translate 0 rotate
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+% Vm
+gsave 10 dict begin
+801 294 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+789 289 moveto
+(Vm)
+[10.08 10.8]
+xshow
+end grestore
+end grestore
+
+% Cemitcodes
+gsave 10 dict begin
+1427 200 46 18 ellipse_path
+stroke
+gsave 10 dict begin
+1393 195 moveto
+(Cemitcodes)
+[9.36 6.24 10.8 3.84 3.84 6.24 6.96 6.96 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Vm -> Cemitcodes
+newpath 826 287 moveto
+871 276 969 254 1053 254 curveto
+1053 254 1053 254 1174 254 curveto
+1249 254 1332 231 1382 215 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1383 218 moveto
+1392 212 lineto
+1381 212 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1383 218 moveto
+1392 212 lineto
+1381 212 lineto
+closepath
+stroke
+end grestore
+
+% Conv_oracle
+gsave 10 dict begin
+1053 300 48 18 ellipse_path
+stroke
+gsave 10 dict begin
+1017 295 moveto
+(Conv_oracle)
+[9.36 6.96 6.48 6.96 6.96 6.96 4.56 6.24 6.24 3.84 6.24]
+xshow
+end grestore
+end grestore
+
+% Vm -> Conv_oracle
+newpath 828 295 moveto
+868 296 942 298 995 299 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 995 303 moveto
+1005 299 lineto
+995 296 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 995 303 moveto
+1005 299 lineto
+995 296 lineto
+closepath
+stroke
+end grestore
+
+% Mod_subst
+gsave 10 dict begin
+1556 146 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+1524 141 moveto
+(Mod_subst)
+[12.48 6.96 6.96 6.96 5.52 6.96 6.96 5.28 3.84]
+xshow
+end grestore
+end grestore
+
+% Cemitcodes -> Mod_subst
+newpath 1459 187 moveto
+1476 180 1497 171 1516 163 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1517 166 moveto
+1525 159 lineto
+1514 160 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1517 166 moveto
+1525 159 lineto
+1514 160 lineto
+closepath
+stroke
+end grestore
+
+% Cbytecodes
+gsave 10 dict begin
+1556 200 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+1523 195 moveto
+(Cbytecodes)
+[9.36 6.48 6.96 3.84 6.24 6.24 6.96 6.96 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Cemitcodes -> Cbytecodes
+newpath 1474 200 moveto
+1482 200 1491 200 1500 200 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1500 204 moveto
+1510 200 lineto
+1500 197 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1500 204 moveto
+1510 200 lineto
+1500 197 lineto
+closepath
+stroke
+end grestore
+
+% Copcodes
+gsave 10 dict begin
+1556 254 41 18 ellipse_path
+stroke
+gsave 10 dict begin
+1528 249 moveto
+(Copcodes)
+[9.36 6.96 6.96 6.24 6.96 6.96 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Cemitcodes -> Copcodes
+newpath 1459 213 moveto
+1476 221 1498 230 1517 237 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1515 240 moveto
+1526 241 lineto
+1518 234 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1515 240 moveto
+1526 241 lineto
+1518 234 lineto
+closepath
+stroke
+end grestore
+
+% Names
+gsave 10 dict begin
+1865 270 33 18 ellipse_path
+stroke
+gsave 10 dict begin
+1845 265 moveto
+(Names)
+[9.6 6.24 10.8 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Conv_oracle -> Names
+newpath 1102 300 moveto
+1151 300 1228 300 1295 300 curveto
+1295 300 1295 300 1666 300 curveto
+1722 300 1785 288 1825 279 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1826 282 moveto
+1835 277 lineto
+1825 276 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1826 282 moveto
+1835 277 lineto
+1825 276 lineto
+closepath
+stroke
+end grestore
+
+% Vconv
+gsave 10 dict begin
+552 202 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+533 197 moveto
+(Vconv)
+[10.08 6.24 6.96 6.48 6.96]
+xshow
+end grestore
+end grestore
+
+% Csymtable
+gsave 10 dict begin
+674 202 43 18 ellipse_path
+stroke
+gsave 10 dict begin
+643 197 moveto
+(Csymtable)
+[9.36 5.52 6.96 10.8 4.08 6.24 6.96 3.84 6.24]
+xshow
+end grestore
+end grestore
+
+% Vconv -> Csymtable
+newpath 584 202 moveto
+595 202 608 202 620 202 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 620 206 moveto
+630 202 lineto
+620 199 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 620 206 moveto
+630 202 lineto
+620 199 lineto
+closepath
+stroke
+end grestore
+
+% Inductive
+gsave 10 dict begin
+674 110 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+647 105 moveto
+(Inductive)
+[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24]
+xshow
+end grestore
+end grestore
+
+% Vconv -> Inductive
+newpath 571 187 moveto
+591 172 622 149 645 132 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 647 135 moveto
+653 126 lineto
+643 129 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 647 135 moveto
+653 126 lineto
+643 129 lineto
+closepath
+stroke
+end grestore
+
+% Csymtable -> Vm
+newpath 696 218 moveto
+717 234 751 258 775 275 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 773 278 moveto
+783 281 lineto
+777 272 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 773 278 moveto
+783 281 lineto
+777 272 lineto
+closepath
+stroke
+end grestore
+
+% Cbytegen
+gsave 10 dict begin
+801 164 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+774 159 moveto
+(Cbytegen)
+[9.36 6.48 6.96 3.84 6.24 6.72 6.24 6.96]
+xshow
+end grestore
+end grestore
+
+% Csymtable -> Cbytegen
+newpath 709 191 moveto
+724 187 742 181 758 177 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 759 180 moveto
+768 174 lineto
+757 174 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 759 180 moveto
+768 174 lineto
+757 174 lineto
+closepath
+stroke
+end grestore
+
+% Type_errors
+gsave 10 dict begin
+801 110 47 18 ellipse_path
+stroke
+gsave 10 dict begin
+767 105 moveto
+(Type_errors)
+[6.96 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
+
+% Inductive -> Type_errors
+newpath 714 110 moveto
+724 110 734 110 744 110 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 744 114 moveto
+754 110 lineto
+744 107 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 744 114 moveto
+754 110 lineto
+744 107 lineto
+closepath
+stroke
+end grestore
+
+% Univ
+gsave 10 dict begin
+1763 241 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+1748 236 moveto
+(Univ)
+[9.6 6.96 3.84 6.96]
+xshow
+end grestore
+end grestore
+
+% Univ -> Names
+newpath 1788 248 moveto
+1800 251 1814 255 1826 259 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1825 262 moveto
+1836 262 lineto
+1827 256 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1825 262 moveto
+1836 262 lineto
+1827 256 lineto
+closepath
+stroke
+end grestore
+
+% Typeops
+gsave 10 dict begin
+552 110 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+528 105 moveto
+(Typeops)
+[6.96 6.96 6.96 6.24 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Typeops -> Inductive
+newpath 589 110 moveto
+600 110 612 110 624 110 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 624 114 moveto
+634 110 lineto
+624 107 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 624 114 moveto
+634 110 lineto
+624 107 lineto
+closepath
+stroke
+end grestore
+
+% Entries
+gsave 10 dict begin
+801 56 33 18 ellipse_path
+stroke
+gsave 10 dict begin
+780 51 moveto
+(Entries)
+[8.4 6.96 3.84 4.8 3.84 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Typeops -> Entries
+newpath 581 99 moveto
+595 93 614 87 630 83 curveto
+673 73 723 66 758 61 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 758 64 moveto
+768 60 lineto
+758 58 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 758 64 moveto
+768 60 lineto
+758 58 lineto
+closepath
+stroke
+end grestore
+
+% Sign
+gsave 10 dict begin
+1427 100 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+1414 95 moveto
+(Sign)
+[7.68 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Entries -> Sign
+newpath 834 61 moveto
+882 68 974 79 1053 79 curveto
+1053 79 1053 79 1174 79 curveto
+1251 79 1342 89 1390 95 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1390 98 moveto
+1400 96 lineto
+1390 92 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1390 98 moveto
+1400 96 lineto
+1390 92 lineto
+closepath
+stroke
+end grestore
+
+% Reduction
+gsave 10 dict begin
+926 208 42 18 ellipse_path
+stroke
+gsave 10 dict begin
+897 203 moveto
+(Reduction)
+[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Type_errors -> Reduction
+newpath 829 125 moveto
+836 129 842 133 848 137 curveto
+868 151 887 170 902 184 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 900 187 moveto
+910 191 lineto
+905 182 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 900 187 moveto
+910 191 lineto
+905 182 lineto
+closepath
+stroke
+end grestore
+
+% Reduction -> Conv_oracle
+newpath 948 224 moveto
+968 239 999 261 1023 278 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1021 281 moveto
+1031 284 lineto
+1025 275 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1021 281 moveto
+1031 284 lineto
+1025 275 lineto
+closepath
+stroke
+end grestore
+
+% Closure
+gsave 10 dict begin
+1053 208 35 18 ellipse_path
+stroke
+gsave 10 dict begin
+1031 203 moveto
+(Closure)
+[9.36 3.84 6.96 5.52 6.96 4.56 6.24]
+xshow
+end grestore
+end grestore
+
+% Reduction -> Closure
+newpath 968 208 moveto
+981 208 994 208 1008 208 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1008 212 moveto
+1018 208 lineto
+1008 205 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1008 212 moveto
+1018 208 lineto
+1008 205 lineto
+closepath
+stroke
+end grestore
+
+% Term_typing
+gsave 10 dict begin
+313 110 49 18 ellipse_path
+stroke
+gsave 10 dict begin
+277 105 moveto
+(Term_typing)
+[7.2 6.24 4.8 10.8 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Term_typing -> Cbytegen
+newpath 347 123 moveto
+363 128 381 134 398 137 curveto
+524 161 675 165 752 165 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 752 169 moveto
+762 165 lineto
+752 162 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 752 169 moveto
+762 165 lineto
+752 162 lineto
+closepath
+stroke
+end grestore
+
+% Cooking
+gsave 10 dict begin
+436 225 37 18 ellipse_path
+stroke
+gsave 10 dict begin
+411 220 moveto
+(Cooking)
+[9.36 6.96 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Term_typing -> Cooking
+newpath 331 127 moveto
+352 147 387 179 410 202 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 408 205 moveto
+418 209 lineto
+413 200 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 408 205 moveto
+418 209 lineto
+413 200 lineto
+closepath
+stroke
+end grestore
+
+% Indtypes
+gsave 10 dict begin
+436 110 37 18 ellipse_path
+stroke
+gsave 10 dict begin
+411 105 moveto
+(Indtypes)
+[4.56 6.96 6.96 3.84 6.96 6.96 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Term_typing -> Indtypes
+newpath 362 110 moveto
+370 110 379 110 388 110 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 388 114 moveto
+398 110 lineto
+388 107 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 388 114 moveto
+398 110 lineto
+388 107 lineto
+closepath
+stroke
+end grestore
+
+% Environ
+gsave 10 dict begin
+1174 181 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+1151 176 moveto
+(Environ)
+[8.4 6.48 6.96 3.84 4.56 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Cbytegen -> Environ
+newpath 841 166 moveto
+911 169 1054 175 1128 179 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1128 183 moveto
+1138 179 lineto
+1128 176 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1128 183 moveto
+1138 179 lineto
+1128 176 lineto
+closepath
+stroke
+end grestore
+
+% Cooking -> Reduction
+newpath 473 227 moveto
+485 228 498 229 510 229 curveto
+603 231 626 233 718 229 curveto
+773 226 834 220 876 214 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 876 217 moveto
+886 213 lineto
+876 211 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 876 217 moveto
+886 213 lineto
+876 211 lineto
+closepath
+stroke
+end grestore
+
+% Indtypes -> Typeops
+newpath 474 110 moveto
+484 110 495 110 505 110 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 505 114 moveto
+515 110 lineto
+505 107 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 505 114 moveto
+515 110 lineto
+505 107 lineto
+closepath
+stroke
+end grestore
+
+% Term
+gsave 10 dict begin
+1666 173 28 18 ellipse_path
+stroke
+gsave 10 dict begin
+1651 168 moveto
+(Term)
+[7.2 6.24 4.8 10.8]
+xshow
+end grestore
+end grestore
+
+% Term -> Univ
+newpath 1685 186 moveto
+1699 196 1719 211 1736 222 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1734 225 moveto
+1744 228 lineto
+1738 219 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1734 225 moveto
+1744 228 lineto
+1738 219 lineto
+closepath
+stroke
+end grestore
+
+% Esubst
+gsave 10 dict begin
+1763 173 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+1743 168 moveto
+(Esubst)
+[8.4 5.52 6.96 6.96 5.28 3.84]
+xshow
+end grestore
+end grestore
+
+% Term -> Esubst
+newpath 1694 173 moveto
+1702 173 1711 173 1720 173 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1720 177 moveto
+1730 173 lineto
+1720 170 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1720 177 moveto
+1730 173 lineto
+1720 170 lineto
+closepath
+stroke
+end grestore
+
+% Subtyping
+gsave 10 dict begin
+552 56 42 18 ellipse_path
+stroke
+gsave 10 dict begin
+523 51 moveto
+(Subtyping)
+[7.68 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Subtyping -> Inductive
+newpath 581 69 moveto
+597 77 618 86 636 93 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 634 96 moveto
+645 97 lineto
+637 90 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 634 96 moveto
+645 97 lineto
+637 90 lineto
+closepath
+stroke
+end grestore
+
+% Modops
+gsave 10 dict begin
+674 18 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+650 13 moveto
+(Modops)
+[12.48 6.96 6.96 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Subtyping -> Modops
+newpath 586 45 moveto
+601 41 618 35 633 31 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 634 34 moveto
+643 28 lineto
+632 28 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 634 34 moveto
+643 28 lineto
+632 28 lineto
+closepath
+stroke
+end grestore
+
+% Modops -> Entries
+newpath 705 27 moveto
+722 32 743 39 761 44 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 760 47 moveto
+771 47 lineto
+762 41 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 760 47 moveto
+771 47 lineto
+762 41 lineto
+closepath
+stroke
+end grestore
+
+% Modops -> Cbytegen
+newpath 686 35 moveto
+695 48 707 67 718 83 curveto
+735 107 733 118 754 137 curveto
+757 140 761 143 765 145 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 763 148 moveto
+773 151 lineto
+767 142 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 763 148 moveto
+773 151 lineto
+767 142 lineto
+closepath
+stroke
+end grestore
+
+% Sign -> Term
+newpath 1454 99 moveto
+1489 98 1553 100 1602 119 curveto
+1626 129 1637 135 1649 148 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1647 151 moveto
+1656 156 lineto
+1652 146 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1647 151 moveto
+1656 156 lineto
+1652 146 lineto
+closepath
+stroke
+end grestore
+
+% Safe_typing
+gsave 10 dict begin
+47 85 46 18 ellipse_path
+stroke
+gsave 10 dict begin
+13 80 moveto
+(Safe_typing)
+[7.68 6.24 4.08 6.24 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Mod_typing
+gsave 10 dict begin
+179 85 48 18 ellipse_path
+stroke
+gsave 10 dict begin
+143 80 moveto
+(Mod_typing)
+[12.48 6.96 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Safe_typing -> Mod_typing
+newpath 94 85 moveto
+103 85 111 85 120 85 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 120 89 moveto
+130 85 lineto
+120 82 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 120 89 moveto
+130 85 lineto
+120 82 lineto
+closepath
+stroke
+end grestore
+
+% Mod_typing -> Term_typing
+newpath 223 93 moveto
+235 95 248 98 260 100 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 260 103 moveto
+270 102 lineto
+261 97 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 260 103 moveto
+270 102 lineto
+261 97 lineto
+closepath
+stroke
+end grestore
+
+% Mod_typing -> Subtyping
+newpath 227 81 moveto
+297 75 428 65 500 60 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 500 63 moveto
+510 59 lineto
+500 57 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 500 63 moveto
+510 59 lineto
+500 57 lineto
+closepath
+stroke
+end grestore
+
+% Closure -> Environ
+newpath 1085 201 moveto
+1099 198 1116 194 1131 190 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1132 193 moveto
+1141 188 lineto
+1131 187 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1132 193 moveto
+1141 188 lineto
+1131 187 lineto
+closepath
+stroke
+end grestore
+
+% Mod_subst -> Term
+newpath 1594 155 moveto
+1606 158 1618 161 1630 164 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1630 167 moveto
+1640 166 lineto
+1631 161 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1630 167 moveto
+1640 166 lineto
+1631 161 lineto
+closepath
+stroke
+end grestore
+
+% Declarations
+gsave 10 dict begin
+1295 181 49 18 ellipse_path
+stroke
+gsave 10 dict begin
+1259 176 moveto
+(Declarations)
+[10.08 6.24 6.24 3.84 6.24 4.56 6.24 3.84 3.84 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Environ -> Declarations
+newpath 1210 181 moveto
+1218 181 1227 181 1236 181 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1236 185 moveto
+1246 181 lineto
+1236 178 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1236 185 moveto
+1246 181 lineto
+1236 178 lineto
+closepath
+stroke
+end grestore
+
+% Declarations -> Cemitcodes
+newpath 1341 188 moveto
+1351 189 1363 191 1373 192 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1373 195 moveto
+1383 194 lineto
+1374 189 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1373 195 moveto
+1383 194 lineto
+1374 189 lineto
+closepath
+stroke
+end grestore
+
+% Declarations -> Sign
+newpath 1320 165 moveto
+1343 152 1375 132 1398 118 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1401 120 moveto
+1407 112 lineto
+1397 115 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1401 120 moveto
+1407 112 lineto
+1397 115 lineto
+closepath
+stroke
+end grestore
+
+% Cbytecodes -> Term
+newpath 1595 190 moveto
+1607 188 1619 185 1630 182 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1631 185 moveto
+1640 179 lineto
+1629 179 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1631 185 moveto
+1640 179 lineto
+1629 179 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF
diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll
new file mode 100644
index 00000000..617163e7
--- /dev/null
+++ b/dev/ocamlweb-doc/lex.mll
@@ -0,0 +1,81 @@
+
+{
+ 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
new file mode 100644
index 00000000..1c68240e
--- /dev/null
+++ b/dev/ocamlweb-doc/library.dep.ps
@@ -0,0 +1,836 @@
+%!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 207
+%%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 207
+%%PageOrientation: Portrait
+gsave
+35 35 542 172 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0.6750 set_scale
+0 0 translate 0 rotate
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+% States
+gsave 10 dict begin
+30 18 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+13 13 moveto
+(States)
+[7.44 4.08 6.24 3.84 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Library
+gsave 10 dict begin
+132 18 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+110 13 moveto
+(Library)
+[8.4 3.84 6.96 4.56 6.24 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+% States -> Library
+newpath 60 18 moveto
+69 18 78 18 87 18 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 87 22 moveto
+97 18 lineto
+87 15 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 87 22 moveto
+97 18 lineto
+87 15 lineto
+closepath
+stroke
+end grestore
+
+% Declaremods
+gsave 10 dict begin
+274 18 50 18 ellipse_path
+stroke
+gsave 10 dict begin
+236 13 moveto
+(Declaremods)
+[10.08 6.24 6.24 3.84 6.24 4.56 6.24 10.8 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Library -> Declaremods
+newpath 167 18 moveto
+181 18 197 18 213 18 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 213 22 moveto
+223 18 lineto
+213 15 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 213 22 moveto
+223 18 lineto
+213 15 lineto
+closepath
+stroke
+end grestore
+
+% Nametab
+gsave 10 dict begin
+523 134 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+497 129 moveto
+(Nametab)
+[9.6 6.24 10.8 6 4.08 6.24 6.96]
+xshow
+end grestore
+end grestore
+
+% Libnames
+gsave 10 dict begin
+642 134 41 18 ellipse_path
+stroke
+gsave 10 dict begin
+613 129 moveto
+(Libnames)
+[8.4 3.84 6.96 6.96 6.24 10.8 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Nametab -> Libnames
+newpath 562 134 moveto
+571 134 580 134 590 134 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 590 138 moveto
+600 134 lineto
+590 131 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 590 138 moveto
+600 134 lineto
+590 131 lineto
+closepath
+stroke
+end grestore
+
+% Summary
+gsave 10 dict begin
+642 65 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+614 60 moveto
+(Summary)
+[7.68 6.96 10.8 10.8 6.24 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+% Nametab -> Summary
+newpath 547 120 moveto
+565 110 589 96 608 84 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 610 87 moveto
+617 79 lineto
+607 81 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 610 87 moveto
+617 79 lineto
+607 81 lineto
+closepath
+stroke
+end grestore
+
+% Nameops
+gsave 10 dict begin
+760 134 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+733 129 moveto
+(Nameops)
+[9.6 6.24 10.8 6.24 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Libnames -> Nameops
+newpath 684 134 moveto
+693 134 701 134 710 134 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 710 138 moveto
+720 134 lineto
+710 131 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 710 138 moveto
+720 134 lineto
+710 131 lineto
+closepath
+stroke
+end grestore
+
+% Lib
+gsave 10 dict begin
+413 153 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+402 148 moveto
+(Lib)
+[8.4 3.84 6.96]
+xshow
+end grestore
+end grestore
+
+% Declaremods -> Lib
+newpath 315 29 moveto
+325 33 336 38 344 45 curveto
+359 58 383 99 399 127 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 396 129 moveto
+404 136 lineto
+402 126 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 396 129 moveto
+404 136 lineto
+402 126 lineto
+closepath
+stroke
+end grestore
+
+% Global
+gsave 10 dict begin
+413 65 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+393 60 moveto
+(Global)
+[10.08 3.84 6.96 6.96 6.24 3.84]
+xshow
+end grestore
+end grestore
+
+% Declaremods -> Global
+newpath 311 30 moveto
+331 37 355 45 375 52 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 374 55 moveto
+385 55 lineto
+376 49 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 374 55 moveto
+385 55 lineto
+376 49 lineto
+closepath
+stroke
+end grestore
+
+% Libobject
+gsave 10 dict begin
+523 188 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+495 183 moveto
+(Libobject)
+[8.4 3.84 6.96 6.96 6.96 3.84 6.24 6.24 3.84]
+xshow
+end grestore
+end grestore
+
+% Libobject -> Libnames
+newpath 552 175 moveto
+567 168 587 159 604 151 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 605 154 moveto
+613 147 lineto
+602 148 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 605 154 moveto
+613 147 lineto
+602 148 lineto
+closepath
+stroke
+end grestore
+
+% Lib -> Nametab
+newpath 439 148 moveto
+450 146 464 144 476 142 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 477 145 moveto
+486 140 lineto
+476 139 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 477 145 moveto
+486 140 lineto
+476 139 lineto
+closepath
+stroke
+end grestore
+
+% Lib -> Libobject
+newpath 437 161 moveto
+450 165 466 170 480 174 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 479 177 moveto
+490 177 lineto
+481 171 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 479 177 moveto
+490 177 lineto
+481 171 lineto
+closepath
+stroke
+end grestore
+
+% Impargs
+gsave 10 dict begin
+274 126 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+251 121 moveto
+(Impargs)
+[4.56 10.56 6.96 6.24 4.32 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Impargs -> Lib
+newpath 308 133 moveto
+329 137 355 142 377 146 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 377 149 moveto
+387 148 lineto
+378 143 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 377 149 moveto
+387 148 lineto
+378 143 lineto
+closepath
+stroke
+end grestore
+
+% Impargs -> Global
+newpath 304 116 moveto
+316 111 331 105 344 99 curveto
+357 94 369 88 381 82 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 382 85 moveto
+390 78 lineto
+379 79 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 382 85 moveto
+390 78 lineto
+379 79 lineto
+closepath
+stroke
+end grestore
+
+% Global -> Libnames
+newpath 443 73 moveto
+473 81 522 94 564 107 curveto
+576 111 589 115 600 119 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 599 122 moveto
+610 122 lineto
+601 116 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 599 122 moveto
+610 122 lineto
+601 116 lineto
+closepath
+stroke
+end grestore
+
+% Global -> Summary
+newpath 446 65 moveto
+484 65 547 65 591 65 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 591 69 moveto
+601 65 lineto
+591 62 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 591 69 moveto
+601 65 lineto
+591 62 lineto
+closepath
+stroke
+end grestore
+
+% Goptions
+gsave 10 dict begin
+274 180 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+248 175 moveto
+(Goptions)
+[10.08 6.96 6.96 3.84 3.84 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Goptions -> Lib
+newpath 310 173 moveto
+331 169 356 164 377 160 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 378 163 moveto
+387 158 lineto
+377 157 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 378 163 moveto
+387 158 lineto
+377 157 lineto
+closepath
+stroke
+end grestore
+
+% Dischargedhypsmap
+gsave 10 dict begin
+274 234 70 18 ellipse_path
+stroke
+gsave 10 dict begin
+217 229 moveto
+(Dischargedhypsmap)
+[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24 6.96 6.48 6.96 6.96 5.52 10.8 6.24 6.96]
+xshow
+end grestore
+end grestore
+
+% Dischargedhypsmap -> Lib
+newpath 317 220 moveto
+326 216 336 212 344 207 curveto
+360 197 376 185 389 175 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 392 177 moveto
+397 168 lineto
+387 172 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 392 177 moveto
+397 168 lineto
+387 172 lineto
+closepath
+stroke
+end grestore
+
+% Declare
+gsave 10 dict begin
+132 126 35 18 ellipse_path
+stroke
+gsave 10 dict begin
+109 121 moveto
+(Declare)
+[10.08 6.24 6.24 3.84 6.24 4.56 6.24]
+xshow
+end grestore
+end grestore
+
+% Declare -> Impargs
+newpath 168 126 moveto
+186 126 208 126 228 126 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 228 130 moveto
+238 126 lineto
+228 123 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 228 130 moveto
+238 126 lineto
+228 123 lineto
+closepath
+stroke
+end grestore
+
+% Declare -> Dischargedhypsmap
+newpath 144 143 moveto
+157 161 179 189 204 207 curveto
+209 210 215 213 221 216 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 219 219 moveto
+230 220 lineto
+222 213 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 219 219 moveto
+230 220 lineto
+222 213 lineto
+closepath
+stroke
+end grestore
+
+% Decl_kinds
+gsave 10 dict begin
+274 72 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+241 67 moveto
+(Decl_kinds)
+[10.08 6.24 6.24 3.84 6.96 6.96 3.84 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+% Declare -> Decl_kinds
+newpath 161 115 moveto
+181 107 209 97 232 88 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 233 91 moveto
+241 84 lineto
+230 85 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 233 91 moveto
+241 84 lineto
+230 85 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF
diff --git a/dev/ocamlweb-doc/macros.tex b/dev/ocamlweb-doc/macros.tex
new file mode 100644
index 00000000..6beacf7b
--- /dev/null
+++ b/dev/ocamlweb-doc/macros.tex
@@ -0,0 +1,7 @@
+
+% 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
new file mode 100644
index 00000000..e537b1f2
--- /dev/null
+++ b/dev/ocamlweb-doc/parse.ml
@@ -0,0 +1,183 @@
+
+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
new file mode 100644
index 00000000..723d8c69
--- /dev/null
+++ b/dev/ocamlweb-doc/parsing.dep.ps
@@ -0,0 +1,1115 @@
+%!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
new file mode 100644
index 00000000..2cd21f02
--- /dev/null
+++ b/dev/ocamlweb-doc/preamble.tex
@@ -0,0 +1,8 @@
+\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
new file mode 100644
index 00000000..02d1b8b5
--- /dev/null
+++ b/dev/ocamlweb-doc/pretyping.dep.ps
@@ -0,0 +1,1259 @@
+%!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
new file mode 100644
index 00000000..0e78f422
--- /dev/null
+++ b/dev/ocamlweb-doc/proofs.dep.ps
@@ -0,0 +1,638 @@
+%!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 136
+%%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 136
+%%PageOrientation: Portrait
+gsave
+35 35 542 101 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0.6923 set_scale
+0 0 translate 0 rotate
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+% Tactic_debug
+gsave 10 dict begin
+163 72 51 18 ellipse_path
+stroke
+gsave 10 dict begin
+125 67 moveto
+(Tactic_debug)
+[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+% Refiner
+gsave 10 dict begin
+287 72 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+266 67 moveto
+(Refiner)
+[9.12 6.24 4.8 3.84 6.96 6.24 4.56]
+xshow
+end grestore
+end grestore
+
+% Tactic_debug -> Refiner
+newpath 214 72 moveto
+223 72 233 72 243 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 243 76 moveto
+253 72 lineto
+243 69 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 243 76 moveto
+253 72 lineto
+243 69 lineto
+closepath
+stroke
+end grestore
+
+% Logic
+gsave 10 dict begin
+390 72 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+373 67 moveto
+(Logic)
+[8.4 6.96 6.96 3.84 6.24]
+xshow
+end grestore
+end grestore
+
+% Refiner -> Logic
+newpath 321 72 moveto
+330 72 340 72 350 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 350 76 moveto
+360 72 lineto
+350 69 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 350 76 moveto
+360 72 lineto
+350 69 lineto
+closepath
+stroke
+end grestore
+
+% Tacmach
+gsave 10 dict begin
+163 126 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+137 121 moveto
+(Tacmach)
+[7.44 6.24 6.24 10.8 6.24 6 6.96]
+xshow
+end grestore
+end grestore
+
+% Tacmach -> Refiner
+newpath 191 114 moveto
+209 106 232 96 251 88 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 253 91 moveto
+261 84 lineto
+250 84 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 253 91 moveto
+261 84 lineto
+250 84 lineto
+closepath
+stroke
+end grestore
+
+% Redexpr
+gsave 10 dict begin
+287 126 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+263 121 moveto
+(Redexpr)
+[9.12 6.24 6.96 5.76 6.96 6.96 4.56]
+xshow
+end grestore
+end grestore
+
+% Tacmach -> Redexpr
+newpath 202 126 moveto
+214 126 227 126 240 126 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 240 130 moveto
+250 126 lineto
+240 123 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 240 130 moveto
+250 126 lineto
+240 123 lineto
+closepath
+stroke
+end grestore
+
+% Proof_trees
+gsave 10 dict begin
+502 72 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+469 67 moveto
+(Proof_trees)
+[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+% Logic -> Proof_trees
+newpath 420 72 moveto
+428 72 437 72 446 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 446 76 moveto
+456 72 lineto
+446 69 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 446 76 moveto
+456 72 lineto
+446 69 lineto
+closepath
+stroke
+end grestore
+
+% Proof_type
+gsave 10 dict begin
+628 72 44 18 ellipse_path
+stroke
+gsave 10 dict begin
+597 67 moveto
+(Proof_type)
+[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24]
+xshow
+end grestore
+end grestore
+
+% Tacexpr
+gsave 10 dict begin
+744 72 35 18 ellipse_path
+stroke
+gsave 10 dict begin
+721 67 moveto
+(Tacexpr)
+[7.44 6.24 6.24 5.76 6.96 6.96 4.56]
+xshow
+end grestore
+end grestore
+
+% Proof_type -> Tacexpr
+newpath 672 72 moveto
+680 72 689 72 698 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 698 76 moveto
+708 72 lineto
+698 69 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 698 76 moveto
+708 72 lineto
+698 69 lineto
+closepath
+stroke
+end grestore
+
+% Proof_trees -> Proof_type
+newpath 548 72 moveto
+557 72 565 72 574 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 574 76 moveto
+584 72 lineto
+574 69 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 574 76 moveto
+584 72 lineto
+574 69 lineto
+closepath
+stroke
+end grestore
+
+% Pfedit
+gsave 10 dict begin
+38 112 29 18 ellipse_path
+stroke
+gsave 10 dict begin
+21 107 moveto
+(Pfedit)
+[7.68 4.08 6.24 6.96 3.84 3.84]
+xshow
+end grestore
+end grestore
+
+% Pfedit -> Tacmach
+newpath 67 115 moveto
+81 117 99 118 115 120 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 115 123 moveto
+125 122 lineto
+116 117 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 115 123 moveto
+125 122 lineto
+116 117 lineto
+closepath
+stroke
+end grestore
+
+% Evar_refiner
+gsave 10 dict begin
+163 18 49 18 ellipse_path
+stroke
+gsave 10 dict begin
+127 13 moveto
+(Evar_refiner)
+[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56]
+xshow
+end grestore
+end grestore
+
+% Pfedit -> Evar_refiner
+newpath 53 96 moveto
+67 82 90 60 112 45 curveto
+116 42 120 40 124 37 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 126 40 moveto
+133 32 lineto
+123 34 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 126 40 moveto
+133 32 lineto
+123 34 lineto
+closepath
+stroke
+end grestore
+
+% Evar_refiner -> Refiner
+newpath 195 32 moveto
+212 40 233 49 251 57 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 249 60 moveto
+260 61 lineto
+252 54 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 249 60 moveto
+260 61 lineto
+252 54 lineto
+closepath
+stroke
+end grestore
+
+% Clenvtac
+gsave 10 dict begin
+38 45 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+13 40 moveto
+(Clenvtac)
+[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24]
+xshow
+end grestore
+end grestore
+
+% Clenvtac -> Tacmach
+newpath 58 61 moveto
+73 72 93 87 112 99 curveto
+117 102 123 105 128 108 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 127 111 moveto
+137 113 lineto
+130 105 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 127 111 moveto
+137 113 lineto
+130 105 lineto
+closepath
+stroke
+end grestore
+
+% Clenvtac -> Evar_refiner
+newpath 73 37 moveto
+85 35 98 32 110 29 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 111 32 moveto
+120 27 lineto
+110 26 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 111 32 moveto
+120 27 lineto
+110 26 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF
diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly
new file mode 100644
index 00000000..bfc7d5cc
--- /dev/null
+++ b/dev/ocamlweb-doc/syntax.mly
@@ -0,0 +1,224 @@
+%{
+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
new file mode 100644
index 00000000..f4de22b7
--- /dev/null
+++ b/dev/ocamlweb-doc/tactics.dep.ps
@@ -0,0 +1,991 @@
+%!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
new file mode 100644
index 00000000..e0355aac
--- /dev/null
+++ b/dev/ocamlweb-doc/toplevel.dep.ps
@@ -0,0 +1,971 @@
+%!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-31 10:48:54 +0000