aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-21 17:28:07 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-01-21 17:28:07 +0000
commit43795b5e6a5280b20201f3b6cd8fb7fe80491e43 (patch)
treec8df4a9fb4594cb91ff4916f07cbf9dc6557d7df
parentb7af7027d15afa2dee1695792a2658f0df392956 (diff)
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--doc/Makefile2
-rw-r--r--doc/interp.dep.ps583
-rw-r--r--doc/kernel.dep.ps1120
-rw-r--r--doc/library.dep.ps527
-rw-r--r--doc/parsing.dep.ps814
-rw-r--r--doc/pretyping.dep.ps965
-rw-r--r--doc/proofs.dep.ps353
-rw-r--r--doc/tactics.dep.ps679
-rw-r--r--doc/toplevel.dep.ps665
9 files changed, 4417 insertions, 1291 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 9d8ea2ee3..a0bef8976 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -46,7 +46,7 @@ coq.tex::
make -C .. doc/coq.tex
depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
- proofs.dep.ps tactics.dep.ps toplevel.dep.ps
+ proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps
%.dot: ../%
(cd ../$*; ocamldep *.ml *.mli) | ocamldot -lr > $@
diff --git a/doc/interp.dep.ps b/doc/interp.dep.ps
new file mode 100644
index 000000000..b05544812
--- /dev/null
+++ b/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/doc/kernel.dep.ps b/doc/kernel.dep.ps
index a0be6b4ca..3c00121e8 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 88
+%%BoundingBox: 35 35 577 127
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,515 +230,1220 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 88
+%%PageBoundingBox: 36 36 577 127
%%PageOrientation: Portrait
gsave
-35 35 542 53 boxprim clip newpath
+35 35 542 92 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.2736 set_scale
+0.2845 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 88] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
-% Univ
+% Vm
gsave 10 dict begin
-1826 172 28 18 ellipse_path
+801 294 27 18 ellipse_path
stroke
gsave 10 dict begin
-1826 167 moveto 35 -0.5 (Univ) alignedtext
+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
-1931 172 35 18 ellipse_path
+1865 270 33 18 ellipse_path
stroke
gsave 10 dict begin
-1931 167 moveto 48 -0.5 (Names) alignedtext
+1845 265 moveto
+(Names)
+[9.6 6.24 10.8 6.24 5.52]
+xshow
end grestore
end grestore
-% Univ -> Names
-newpath 1855 172 moveto
-1865 172 1875 172 1886 172 curveto
+% 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 1886 170 moveto
-1896 172 lineto
-1886 175 lineto
+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
-% Typeops
+% Vconv
gsave 10 dict begin
-613 149 40 18 ellipse_path
+552 202 32 18 ellipse_path
stroke
gsave 10 dict begin
-613 144 moveto 58 -0.5 (Typeops) alignedtext
+533 197 moveto
+(Vconv)
+[10.08 6.24 6.96 6.48 6.96]
+xshow
end grestore
end grestore
-% Entries
+% Csymtable
gsave 10 dict begin
-872 168 35 18 ellipse_path
+674 202 43 18 ellipse_path
stroke
gsave 10 dict begin
-872 163 moveto 48 -0.5 (Entries) alignedtext
+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
-% Typeops -> Entries
-newpath 653 152 moveto
-701 155 781 161 830 165 curveto
+% 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 827 163 moveto
-837 165 lineto
-827 168 lineto
+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
-739 72 43 18 ellipse_path
+674 110 39 18 ellipse_path
stroke
gsave 10 dict begin
-739 67 moveto 64 -0.5 (Inductive) alignedtext
+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
-% Typeops -> Inductive
-newpath 637 134 moveto
-657 122 685 105 706 92 curveto
+% 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 704 90 moveto
-714 87 lineto
-707 94 lineto
+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
-% Sign
+% 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
-1633 145 27 18 ellipse_path
+801 164 39 18 ellipse_path
stroke
gsave 10 dict begin
-1633 140 moveto 30 -0.5 (Sign) alignedtext
+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
-% Entries -> Sign
-newpath 907 168 moveto
-976 168 1124 167 1147 168 curveto
-1147 168 1147 168 1387 168 curveto
-1462 167 1549 157 1597 150 curveto
+% 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 1597 148 moveto
-1607 149 lineto
-1597 152 lineto
+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
-872 72 53 18 ellipse_path
+801 110 47 18 ellipse_path
stroke
gsave 10 dict begin
-872 67 moveto 85 -0.5 (Type_errors) alignedtext
+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 782 72 moveto
-791 72 799 72 808 72 curveto
+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 808 70 moveto
-818 72 lineto
-808 75 lineto
+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
-1009 72 46 18 ellipse_path
+926 208 42 18 ellipse_path
stroke
gsave 10 dict begin
-1009 67 moveto 71 -0.5 (Reduction) alignedtext
+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 926 72 moveto
-935 72 943 72 952 72 curveto
+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 952 70 moveto
-962 72 lineto
-952 75 lineto
+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
-% Conv_oracle
+% Reduction -> Conv_oracle
+newpath 948 224 moveto
+968 239 999 261 1023 278 curveto
+stroke
gsave 10 dict begin
-1147 74 55 18 ellipse_path
+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
-1147 69 moveto 88 -0.5 (Conv_oracle) alignedtext
+1031 203 moveto
+(Closure)
+[9.36 3.84 6.96 5.52 6.96 4.56 6.24]
+xshow
end grestore
end grestore
-% Reduction -> Conv_oracle
-newpath 1056 73 moveto
-1065 73 1073 73 1082 73 curveto
+% 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 1082 71 moveto
-1092 73 lineto
-1082 76 lineto
+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
-355 95 57 18 ellipse_path
+313 110 49 18 ellipse_path
stroke
gsave 10 dict begin
-355 90 moveto 92 -0.5 (Term_typing) alignedtext
+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
-489 95 40 18 ellipse_path
+436 225 37 18 ellipse_path
stroke
gsave 10 dict begin
-489 90 moveto 58 -0.5 (Cooking) alignedtext
+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 412 95 moveto
-421 95 430 95 439 95 curveto
+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 439 93 moveto
-449 95 lineto
-439 98 lineto
+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
-489 149 40 18 ellipse_path
+436 110 37 18 ellipse_path
stroke
gsave 10 dict begin
-489 144 moveto 59 -0.5 (Indtypes) alignedtext
+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 390 109 moveto
-409 117 432 126 451 134 curveto
+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 451 131 moveto
-459 137 lineto
-449 136 lineto
+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 511 80 moveto
-532 66 560 47 566 45 curveto
-720 0 768 20 926 45 curveto
-935 47 951 52 968 58 curveto
+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 966 55 moveto
-975 60 lineto
-965 60 lineto
+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 530 149 moveto
-541 149 552 149 563 149 curveto
+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 563 147 moveto
-573 149 lineto
-563 152 lineto
+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
-1726 145 30 18 ellipse_path
+1666 173 28 18 ellipse_path
stroke
gsave 10 dict begin
-1726 140 moveto 38 -0.5 (Term) alignedtext
+1651 168 moveto
+(Term)
+[7.2 6.24 4.8 10.8]
+xshow
end grestore
end grestore
% Term -> Univ
-newpath 1754 152 moveto
-1765 155 1779 159 1791 162 curveto
+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 1791 159 moveto
-1800 165 lineto
-1790 164 lineto
+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
-1826 118 33 18 ellipse_path
+1763 173 32 18 ellipse_path
stroke
gsave 10 dict begin
-1826 113 moveto 45 -0.5 (Esubst) alignedtext
+1743 168 moveto
+(Esubst)
+[8.4 5.52 6.96 6.96 5.28 3.84]
+xshow
end grestore
end grestore
% Term -> Esubst
-newpath 1754 138 moveto
-1764 135 1776 132 1787 129 curveto
+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 1786 127 moveto
-1796 126 lineto
-1787 132 lineto
+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
-613 72 46 18 ellipse_path
+552 56 42 18 ellipse_path
stroke
gsave 10 dict begin
-613 67 moveto 71 -0.5 (Subtyping) alignedtext
+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 660 72 moveto
-669 72 677 72 686 72 curveto
+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 686 70 moveto
-696 72 lineto
-686 75 lineto
+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
-739 126 38 18 ellipse_path
+674 18 36 18 ellipse_path
stroke
gsave 10 dict begin
-739 121 moveto 55 -0.5 (Modops) alignedtext
+650 13 moveto
+(Modops)
+[12.48 6.96 6.96 6.96 6.96 5.52]
+xshow
end grestore
end grestore
% Subtyping -> Modops
-newpath 644 85 moveto
-662 93 684 102 702 110 curveto
+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 703 108 moveto
-711 114 lineto
-701 112 lineto
+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 771 136 moveto
-790 142 814 150 833 156 curveto
+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 833 153 moveto
-842 159 lineto
-832 158 lineto
+newpath 760 47 moveto
+771 47 lineto
+762 41 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% Environ
-gsave 10 dict begin
-1387 122 39 18 ellipse_path
+newpath 760 47 moveto
+771 47 lineto
+762 41 lineto
+closepath
stroke
-gsave 10 dict begin
-1387 117 moveto 56 -0.5 (Environ) alignedtext
-end grestore
end grestore
-% Modops -> Environ
-newpath 777 125 moveto
-830 124 926 122 1009 122 curveto
-1009 122 1009 122 1147 122 curveto
-1152 122 1270 122 1339 122 curveto
+% 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 1338 120 moveto
-1348 122 lineto
-1338 125 lineto
+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 1660 145 moveto
-1668 145 1677 145 1686 145 curveto
+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 1686 143 moveto
-1696 145 lineto
-1686 148 lineto
+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
-62 72 53 18 ellipse_path
+47 85 46 18 ellipse_path
stroke
gsave 10 dict begin
-62 67 moveto 85 -0.5 (Safe_typing) alignedtext
+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
-207 72 54 18 ellipse_path
+179 85 48 18 ellipse_path
stroke
gsave 10 dict begin
-207 67 moveto 87 -0.5 (Mod_typing) alignedtext
+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 116 72 moveto
-125 72 133 72 142 72 curveto
+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 142 70 moveto
-152 72 lineto
-142 75 lineto
+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 257 80 moveto
-269 82 282 84 294 86 curveto
+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 294 84 moveto
-304 87 lineto
-294 88 lineto
+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 261 69 moveto
-273 69 286 68 298 68 curveto
-402 66 427 66 530 68 curveto
-536 68 547 69 559 69 curveto
+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 557 66 moveto
-567 70 lineto
-557 71 lineto
+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
-gsave 10 dict begin
-1275 75 37 18 ellipse_path
+% Closure -> Environ
+newpath 1085 201 moveto
+1099 198 1116 194 1131 190 curveto
stroke
gsave 10 dict begin
-1275 70 moveto 52 -0.5 (Closure) alignedtext
-end grestore
+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
-% Conv_oracle -> Closure
-newpath 1202 74 moveto
-1211 74 1220 75 1228 75 curveto
+% 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 1228 73 moveto
-1238 75 lineto
-1228 78 lineto
+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
-1516 122 53 18 ellipse_path
+1295 181 49 18 ellipse_path
stroke
gsave 10 dict begin
-1516 117 moveto 85 -0.5 (Declarations) alignedtext
+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 1426 122 moveto
-1434 122 1443 122 1452 122 curveto
+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 1452 120 moveto
-1462 122 lineto
-1452 125 lineto
+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 1562 131 moveto
-1574 133 1587 136 1598 138 curveto
+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 1598 135 moveto
-1607 140 lineto
-1597 140 lineto
+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
-% Closure -> Environ
-newpath 1303 87 moveto
-1317 93 1334 100 1349 106 curveto
+% 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 1350 104 moveto
-1358 110 lineto
-1348 108 lineto
+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
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index 7ce732adb..1c68240e7 100644
--- a/doc/library.dep.ps
+++ b/doc/library.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 174
+%%BoundingBox: 35 35 577 207
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,376 +230,602 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 174
+%%PageBoundingBox: 36 36 577 207
%%PageOrientation: Portrait
gsave
-35 35 542 139 boxprim clip newpath
+35 35 542 172 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.5444 set_scale
+0.6750 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 174] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
-% Summary
+% States
gsave 10 dict begin
-688 134 45 18 ellipse_path
+30 18 30 18 ellipse_path
stroke
gsave 10 dict begin
-688 129 moveto 69 -0.5 (Summary) alignedtext
+13 13 moveto
+(States)
+[7.44 4.08 6.24 3.84 6.24 5.52]
+xshow
end grestore
end grestore
-% Libnames
+% Library
gsave 10 dict begin
-815 107 44 18 ellipse_path
+132 18 34 18 ellipse_path
stroke
gsave 10 dict begin
-815 102 moveto 67 -0.5 (Libnames) alignedtext
+110 13 moveto
+(Library)
+[8.4 3.84 6.96 4.56 6.24 4.8 6.96]
+xshow
end grestore
end grestore
-% Summary -> Libnames
-newpath 728 125 moveto
-740 123 753 120 765 117 curveto
+% 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 765 115 moveto
-775 115 lineto
-766 119 lineto
+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
-% Nameops
+% Declaremods
gsave 10 dict begin
-940 107 43 18 ellipse_path
+274 18 50 18 ellipse_path
stroke
gsave 10 dict begin
-940 102 moveto 65 -0.5 (Nameops) alignedtext
+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
-% Libnames -> Nameops
-newpath 860 107 moveto
-869 107 877 107 886 107 curveto
+% 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 886 105 moveto
-896 107 lineto
-886 110 lineto
+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
-% States
+% Nametab
gsave 10 dict begin
-38 234 30 18 ellipse_path
+523 134 39 18 ellipse_path
stroke
gsave 10 dict begin
-38 229 moveto 38 -0.5 (States) alignedtext
+497 129 moveto
+(Nametab)
+[9.6 6.24 10.8 6 4.08 6.24 6.96]
+xshow
end grestore
end grestore
-% Library
+% Libnames
gsave 10 dict begin
-142 234 37 18 ellipse_path
+642 134 41 18 ellipse_path
stroke
gsave 10 dict begin
-142 229 moveto 53 -0.5 (Library) alignedtext
+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
-% States -> Library
-newpath 68 234 moveto
-76 234 85 234 94 234 curveto
+% 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 94 232 moveto
-104 234 lineto
-94 237 lineto
+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
-% Declaremods
+% Summary
gsave 10 dict begin
-298 234 55 18 ellipse_path
+642 65 40 18 ellipse_path
stroke
gsave 10 dict begin
-298 229 moveto 89 -0.5 (Declaremods) alignedtext
+614 60 moveto
+(Summary)
+[7.68 6.96 10.8 10.8 6.24 4.8 6.96]
+xshow
end grestore
end grestore
-% Library -> Declaremods
-newpath 180 234 moveto
-196 234 215 234 232 234 curveto
+% 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 232 232 moveto
-242 234 lineto
-232 237 lineto
+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
-% Nametab
+% Nameops
gsave 10 dict begin
-563 126 43 18 ellipse_path
+760 134 40 18 ellipse_path
stroke
gsave 10 dict begin
-563 121 moveto 64 -0.5 (Nametab) alignedtext
+733 129 moveto
+(Nameops)
+[9.6 6.24 10.8 6.24 6.96 6.96 5.52]
+xshow
end grestore
end grestore
-% Nametab -> Summary
-newpath 606 129 moveto
-615 130 624 130 633 130 curveto
+% 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 633 128 moveto
-643 131 lineto
-633 132 lineto
+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
-450 99 27 18 ellipse_path
+413 153 27 18 ellipse_path
stroke
gsave 10 dict begin
-450 94 moveto 23 -0.5 (Lib) alignedtext
+402 148 moveto
+(Lib)
+[8.4 3.84 6.96]
+xshow
end grestore
end grestore
% Declaremods -> Lib
-newpath 346 225 moveto
-358 221 370 215 380 207 curveto
-405 186 399 171 416 145 curveto
-421 138 427 130 432 123 curveto
+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 430 122 moveto
-437 115 lineto
-434 125 lineto
+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
-450 172 33 18 ellipse_path
+413 65 32 18 ellipse_path
stroke
gsave 10 dict begin
-450 167 moveto 45 -0.5 (Global) alignedtext
+393 60 moveto
+(Global)
+[10.08 3.84 6.96 6.96 6.24 3.84]
+xshow
end grestore
end grestore
% Declaremods -> Global
-newpath 337 221 moveto
-358 214 379 207 380 207 curveto
-393 201 406 195 418 189 curveto
+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 416 187 moveto
-426 185 lineto
-418 192 lineto
+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
-688 80 43 18 ellipse_path
+523 188 40 18 ellipse_path
stroke
gsave 10 dict begin
-688 75 moveto 65 -0.5 (Libobject) alignedtext
+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 727 88 moveto
-739 90 753 93 766 96 curveto
+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 767 94 moveto
-776 98 lineto
-766 98 lineto
+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 476 105 moveto
-489 108 504 112 519 115 curveto
+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 517 112 moveto
-526 117 lineto
-516 117 lineto
+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 477 97 moveto
-516 94 589 88 638 84 curveto
+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 635 82 moveto
-645 83 lineto
-635 87 lineto
+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
-298 126 39 18 ellipse_path
+274 126 36 18 ellipse_path
stroke
gsave 10 dict begin
-298 121 moveto 56 -0.5 (Impargs) alignedtext
+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 334 120 moveto
-359 116 391 110 415 105 curveto
+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 414 103 moveto
-424 104 lineto
-414 108 lineto
+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 331 136 moveto
-355 143 387 153 412 161 curveto
+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 412 158 moveto
-421 163 lineto
-411 163 lineto
+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 483 169 moveto
-515 166 564 160 606 153 curveto
-617 151 629 148 640 146 curveto
+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 639 144 moveto
-649 144 lineto
-640 149 lineto
+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
-298 72 42 18 ellipse_path
+274 180 39 18 ellipse_path
stroke
gsave 10 dict begin
-298 67 moveto 62 -0.5 (Goptions) alignedtext
+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 337 79 moveto
-361 83 392 89 415 93 curveto
+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 414 90 moveto
-424 94 lineto
-414 95 lineto
+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
-298 18 81 18 ellipse_path
+274 234 70 18 ellipse_path
stroke
gsave 10 dict begin
-298 13 moveto 141 -0.5 (Dischargedhypsmap) alignedtext
+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 344 33 moveto
-363 39 380 45 380 45 curveto
-397 54 415 68 428 79 curveto
+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 428 76 moveto
-434 84 lineto
-425 80 lineto
+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
-142 126 37 18 ellipse_path
+132 126 35 18 ellipse_path
stroke
gsave 10 dict begin
-142 121 moveto 52 -0.5 (Declare) alignedtext
+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 179 126 moveto
-200 126 227 126 250 126 curveto
+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 249 124 moveto
-259 126 lineto
-249 129 lineto
+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 157 109 moveto
-178 86 213 48 216 45 curveto
-221 42 230 38 241 35 curveto
+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 239 33 moveto
-249 32 lineto
-241 38 lineto
+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
-298 180 50 18 ellipse_path
+274 72 45 18 ellipse_path
stroke
gsave 10 dict begin
-298 175 moveto 78 -0.5 (Decl_kinds) alignedtext
+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 172 137 moveto
-189 143 208 150 216 153 curveto
-228 157 240 161 252 165 curveto
+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 252 162 moveto
-261 168 lineto
-251 167 lineto
+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
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index be76f7404..723d8c697 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 196
+%%BoundingBox: 35 35 577 314
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,480 +230,881 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 196
+%%PageBoundingBox: 36 36 577 314
%%PageOrientation: Portrait
gsave
-35 35 542 161 boxprim clip newpath
+35 35 542 279 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6767 set_scale
+0.6027 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 196] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Pcoq
gsave 10 dict begin
-441 180 27 18 ellipse_path
+557 280 27 18 ellipse_path
stroke
gsave 10 dict begin
-441 175 moveto 33 -0.5 (Pcoq) alignedtext
+543 275 moveto
+(Pcoq)
+[7.68 6.24 6.96 6.96]
+xshow
end grestore
end grestore
% Extend
gsave 10 dict begin
-552 126 35 18 ellipse_path
+664 226 33 18 ellipse_path
stroke
gsave 10 dict begin
-552 121 moveto 49 -0.5 (Extend) alignedtext
+643 221 moveto
+(Extend)
+[8.4 6.96 3.84 6.24 6.96 6.96]
+xshow
end grestore
end grestore
% Pcoq -> Extend
-newpath 463 169 moveto
-478 161 500 151 517 143 curveto
+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 516 141 moveto
-526 139 lineto
-518 145 lineto
+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
-655 72 27 18 ellipse_path
+764 172 27 18 ellipse_path
stroke
gsave 10 dict begin
-655 67 moveto 23 -0.5 (Ast) alignedtext
+753 167 moveto
+(Ast)
+[10.08 5.28 3.84]
+xshow
end grestore
end grestore
% Extend -> Ast
-newpath 577 113 moveto
-591 105 610 96 626 87 curveto
+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 624 85 moveto
-634 83 lineto
-626 90 lineto
+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
-655 126 31 18 ellipse_path
+764 226 29 18 ellipse_path
stroke
gsave 10 dict begin
-655 121 moveto 40 -0.5 (Lexer) alignedtext
+747 221 moveto
+(Lexer)
+[8.4 5.76 6.48 6.24 4.56]
+xshow
end grestore
end grestore
% Extend -> Lexer
-newpath 588 126 moveto
-597 126 606 126 614 126 curveto
+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 614 124 moveto
-624 126 lineto
-614 129 lineto
+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
-441 72 39 18 ellipse_path
+557 172 35 18 ellipse_path
stroke
gsave 10 dict begin
-441 67 moveto 56 -0.5 (Termast) alignedtext
+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 480 72 moveto
-520 72 581 72 620 72 curveto
+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 618 70 moveto
-628 72 lineto
-618 75 lineto
+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
-756 72 34 18 ellipse_path
+863 172 32 18 ellipse_path
stroke
gsave 10 dict begin
-756 67 moveto 46 -0.5 (Coqast) alignedtext
+843 167 moveto
+(Coqast)
+[9.36 6.96 6.96 6.24 5.28 3.84]
+xshow
end grestore
end grestore
% Ast -> Coqast
-newpath 682 72 moveto
-691 72 702 72 712 72 curveto
+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 712 70 moveto
-722 72 lineto
-712 75 lineto
+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
-% Search
+% Tactic_printer
gsave 10 dict begin
-46 122 33 18 ellipse_path
+53 126 52 18 ellipse_path
stroke
gsave 10 dict begin
-46 117 moveto 45 -0.5 (Search) alignedtext
+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
-% Printer
+% Pptactic
gsave 10 dict begin
-169 122 34 18 ellipse_path
+178 126 36 18 ellipse_path
stroke
gsave 10 dict begin
-169 117 moveto 47 -0.5 (Printer) alignedtext
+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
-% Search -> Printer
-newpath 80 122 moveto
-94 122 110 122 124 122 curveto
+% 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 124 120 moveto
-134 122 lineto
-124 125 lineto
+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
-% Ppconstr
+% Printer
gsave 10 dict begin
-310 72 40 18 ellipse_path
+289 72 32 18 ellipse_path
stroke
gsave 10 dict begin
-310 67 moveto 59 -0.5 (Ppconstr) alignedtext
+269 67 moveto
+(Printer)
+[7.68 4.8 3.84 6.96 3.84 6.24 4.56]
+xshow
end grestore
end grestore
-% Printer -> Ppconstr
-newpath 198 112 moveto
-218 105 246 95 269 86 curveto
+% 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 268 84 moveto
-278 83 lineto
-269 89 lineto
+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
-% Ppconstr -> Pcoq
-newpath 340 84 moveto
-351 89 362 95 366 99 curveto
-388 117 382 132 402 153 curveto
-406 157 409 160 413 163 curveto
+% 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 414 161 moveto
-421 168 lineto
-411 165 lineto
+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
-% Ppconstr -> Termast
-newpath 351 72 moveto
-364 72 379 72 392 72 curveto
+% 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 392 70 moveto
-402 72 lineto
-392 75 lineto
+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
-441 126 39 18 ellipse_path
+557 226 36 18 ellipse_path
stroke
gsave 10 dict begin
-441 121 moveto 56 -0.5 (Esyntax) alignedtext
+533 221 moveto
+(Esyntax)
+[8.4 5.52 6.96 6.96 4.08 6.24 6.96]
+xshow
end grestore
end grestore
-% Ppconstr -> Esyntax
-newpath 340 84 moveto
-358 92 383 102 403 110 curveto
+% 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 404 108 moveto
-412 114 lineto
-402 112 lineto
+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
-% Prettyp
+% Ppconstr
gsave 10 dict begin
-46 68 36 18 ellipse_path
+424 388 37 18 ellipse_path
stroke
gsave 10 dict begin
-46 63 moveto 50 -0.5 (Prettyp) alignedtext
+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
-% Prettyp -> Printer
-newpath 73 80 moveto
-91 88 115 98 134 106 curveto
+% 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 134 103 moveto
-142 110 lineto
-132 108 lineto
+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
-% Printmod
+% 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
-169 68 43 18 ellipse_path
+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
-169 63 moveto 65 -0.5 (Printmod) alignedtext
+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 -> Printmod
-newpath 82 68 moveto
-93 68 104 68 115 68 curveto
+% 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 115 66 moveto
-125 68 lineto
-115 71 lineto
+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
-% Pptactic
+% Printmod
gsave 10 dict begin
-46 188 38 18 ellipse_path
+289 18 39 18 ellipse_path
stroke
gsave 10 dict begin
-46 183 moveto 54 -0.5 (Pptactic) alignedtext
+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
-% Pptactic -> Printer
-newpath 71 174 moveto
-90 164 116 150 137 139 curveto
+% 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 135 137 moveto
-145 135 lineto
-137 142 lineto
+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
-% Egrammar
+% G_zsyntax
gsave 10 dict begin
-169 213 48 18 ellipse_path
+424 172 43 18 ellipse_path
stroke
gsave 10 dict begin
-169 208 moveto 75 -0.5 (Egrammar) alignedtext
+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
-% Pptactic -> Egrammar
-newpath 81 195 moveto
-92 197 104 200 116 202 curveto
+% 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 117 200 moveto
-126 204 lineto
-116 204 lineto
+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
-% Egrammar -> Pcoq
-newpath 217 216 moveto
-257 217 316 216 366 207 curveto
-374 205 392 199 407 193 curveto
+% 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 407 190 moveto
-417 189 lineto
-409 195 lineto
+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
-% Esyntax -> Extend
-newpath 480 126 moveto
-489 126 498 126 506 126 curveto
+% 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 506 124 moveto
-516 126 lineto
-506 129 lineto
+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_zsyntax
+% G_string_syntax
gsave 10 dict begin
-310 18 49 18 ellipse_path
+424 280 59 18 ellipse_path
stroke
gsave 10 dict begin
-310 13 moveto 76 -0.5 (G_zsyntax) alignedtext
+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_zsyntax -> Pcoq
-newpath 346 30 moveto
-353 34 361 39 366 45 curveto
-400 82 372 112 402 153 curveto
-405 156 408 160 412 162 curveto
+% 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 413 160 moveto
-420 168 lineto
-411 164 lineto
+newpath 520 284 moveto
+530 280 lineto
+520 277 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% G_zsyntax -> Termast
-newpath 343 31 moveto
-361 39 385 48 404 56 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 404 53 moveto
-412 60 lineto
-402 58 lineto
+newpath 520 284 moveto
+530 280 lineto
+520 277 lineto
closepath
-fill
-0.000 0.000 0.000 edgecolor
+stroke
+end grestore
-% G_zsyntax -> Esyntax
-newpath 342 32 moveto
-352 36 362 41 366 45 curveto
-388 64 382 78 402 99 curveto
-404 101 407 104 409 106 curveto
+% 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 410 104 moveto
-417 112 lineto
-408 108 lineto
+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
-310 180 48 18 ellipse_path
+424 118 42 18 ellipse_path
stroke
gsave 10 dict begin
-310 175 moveto 74 -0.5 (G_rsyntax) alignedtext
+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 358 180 moveto
-373 180 389 180 404 180 curveto
+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 403 178 moveto
-413 180 lineto
-403 183 lineto
+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 342 166 moveto
-352 162 362 157 366 153 curveto
-388 134 382 119 402 99 curveto
-404 96 407 94 409 92 curveto
+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 407 90 moveto
-417 86 lineto
-411 94 lineto
+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 342 167 moveto
-360 159 384 150 403 142 curveto
+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 402 140 moveto
-412 138 lineto
-404 144 lineto
+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
-310 126 56 18 ellipse_path
+424 226 48 18 ellipse_path
stroke
gsave 10 dict begin
-310 121 moveto 90 -0.5 (G_natsyntax) alignedtext
+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 345 140 moveto
-365 149 391 159 410 167 curveto
+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 410 164 moveto
-418 170 lineto
-408 169 lineto
+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 345 112 moveto
-363 104 385 95 403 87 curveto
+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 402 85 moveto
-412 84 lineto
-403 90 lineto
+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 366 126 moveto
-375 126 384 126 392 126 curveto
+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 392 124 moveto
-402 126 lineto
-392 129 lineto
+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
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index ffa9c5302..02d1b8b5a 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 159
+%%BoundingBox: 35 35 577 146
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,537 +230,1025 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 159
+%%PageBoundingBox: 36 36 577 146
%%PageOrientation: Portrait
gsave
-35 35 542 124 boxprim clip newpath
+35 35 542 111 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.3634 set_scale
+0.3600 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 159] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
-% Typing
+% Unification
gsave 10 dict begin
-523 241 36 18 ellipse_path
+610 118 45 18 ellipse_path
stroke
gsave 10 dict begin
-523 236 moveto 50 -0.5 (Typing) alignedtext
+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
-% Pretype_errors
+% Evarutil
gsave 10 dict begin
-898 264 62 18 ellipse_path
+728 72 36 18 ellipse_path
stroke
gsave 10 dict begin
-898 259 moveto 102 -0.5 (Pretype_errors) alignedtext
+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
-% Typing -> Pretype_errors
-newpath 559 243 moveto
-621 247 750 255 830 260 curveto
+% 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 827 258 moveto
-837 260 lineto
-827 263 lineto
+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
-% Rawterm
+% Pattern
gsave 10 dict begin
-1051 114 43 18 ellipse_path
+728 210 33 18 ellipse_path
stroke
gsave 10 dict begin
-1051 109 moveto 65 -0.5 (Rawterm) alignedtext
+708 205 moveto
+(Pattern)
+[7.44 6.24 3.84 3.84 6.24 4.8 6.96]
+xshow
end grestore
end grestore
-% Pretype_errors -> Rawterm
-newpath 939 250 moveto
-946 247 954 242 960 237 curveto
-983 218 979 206 996 183 curveto
-1008 168 1021 151 1032 138 curveto
+% 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 1029 138 moveto
-1037 131 lineto
-1033 141 lineto
+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
-% Inductiveops
+% Retyping
gsave 10 dict begin
-1051 210 54 18 ellipse_path
+839 118 38 18 ellipse_path
stroke
gsave 10 dict begin
-1051 205 moveto 87 -0.5 (Inductiveops) alignedtext
+813 113 moveto
+(Retyping)
+[9.12 6 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
end grestore
end grestore
-% Pretype_errors -> Inductiveops
-newpath 937 250 moveto
-958 243 984 234 1005 226 curveto
+% 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 1004 224 moveto
-1014 223 lineto
-1005 229 lineto
+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
-% Tacred
+% Typing
gsave 10 dict begin
-761 120 34 18 ellipse_path
+839 64 32 18 ellipse_path
stroke
gsave 10 dict begin
-761 115 moveto 47 -0.5 (Tacred) alignedtext
+819 59 moveto
+(Typing)
+[6.96 6.96 6.96 3.84 6.96 6.96]
+xshow
end grestore
end grestore
-% Cbv
+% Evarutil -> Typing
+newpath 764 69 moveto
+775 68 786 67 797 67 curveto
+stroke
gsave 10 dict begin
-1200 18 27 18 ellipse_path
+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
-1200 13 moveto 29 -0.5 (Cbv) alignedtext
+1083 105 moveto
+(Rawterm)
+[9.36 5.76 10.08 3.84 6.24 4.8 10.8]
+xshow
end grestore
end grestore
-% Tacred -> Cbv
-newpath 775 103 moveto
-794 80 828 41 836 37 curveto
-852 30 1077 22 1165 19 curveto
+% 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 1163 17 moveto
-1173 19 lineto
-1163 22 lineto
+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
-% Tacred -> Rawterm
-newpath 796 119 moveto
-847 118 941 116 999 115 curveto
+% 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 997 113 moveto
-1007 115 lineto
-997 118 lineto
+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
-% Retyping
+% Pretype_errors
gsave 10 dict begin
-898 210 43 18 ellipse_path
+969 72 54 18 ellipse_path
stroke
gsave 10 dict begin
-898 205 moveto 64 -0.5 (Retyping) alignedtext
+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
-% Tacred -> Retyping
-newpath 779 135 moveto
-801 154 835 182 836 183 curveto
-837 183 847 188 859 193 curveto
+% 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 860 191 moveto
-868 197 lineto
-858 195 lineto
+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
-% Instantiate
+% Pretype_errors -> Rawterm
+newpath 1011 84 moveto
+1029 88 1048 94 1065 98 curveto
+stroke
gsave 10 dict begin
-1341 18 46 18 ellipse_path
+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
-1341 13 moveto 71 -0.5 (Instantiate) alignedtext
+709 13 moveto
+(Tacred)
+[7.44 6.24 6.24 4.56 6.24 6.96]
+xshow
end grestore
end grestore
-% Cbv -> Instantiate
-newpath 1227 18 moveto
-1243 18 1264 18 1284 18 curveto
+% 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 1284 16 moveto
-1294 18 lineto
-1284 21 lineto
+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
-% Retyping -> Inductiveops
-newpath 941 210 moveto
-955 210 971 210 986 210 curveto
+% 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 986 208 moveto
-996 210 lineto
-986 213 lineto
+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
-% Reductionops
+% Cbv
gsave 10 dict begin
-1200 72 58 18 ellipse_path
+1246 41 27 18 ellipse_path
stroke
gsave 10 dict begin
-1200 67 moveto 94 -0.5 (Reductionops) alignedtext
+1234 36 moveto
+(Cbv)
+[9.36 6.48 6.96]
+xshow
end grestore
end grestore
-% Inductiveops -> Reductionops
-newpath 1070 193 moveto
-1097 169 1146 123 1175 95 curveto
+% 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 1172 94 moveto
-1181 89 lineto
-1176 98 lineto
+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
-% Reductionops -> Instantiate
-newpath 1237 58 moveto
-1256 51 1279 42 1299 34 curveto
+% 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 1298 32 moveto
-1308 31 lineto
-1299 37 lineto
+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
-% Termops
+% Reductionops
gsave 10 dict begin
-1341 72 41 18 ellipse_path
+1246 164 51 18 ellipse_path
stroke
gsave 10 dict begin
-1341 67 moveto 60 -0.5 (Termops) alignedtext
+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
-% Reductionops -> Termops
-newpath 1258 72 moveto
-1269 72 1280 72 1290 72 curveto
+% 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 1290 70 moveto
-1300 72 lineto
-1290 75 lineto
+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
-% Evd
+% Reductionops -> Evd
+newpath 1277 150 moveto
+1294 142 1313 133 1330 125 curveto
+stroke
gsave 10 dict begin
-1451 18 27 18 ellipse_path
+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
-1451 13 moveto 28 -0.5 (Evd) alignedtext
+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
-% Instantiate -> Evd
-newpath 1388 18 moveto
-1397 18 1406 18 1414 18 curveto
+% 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 16 moveto
-1424 18 lineto
-1414 21 lineto
+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
-523 149 47 18 ellipse_path
+485 24 43 18 ellipse_path
stroke
gsave 10 dict begin
-523 144 moveto 72 -0.5 (Recordops) alignedtext
+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
-646 139 39 18 ellipse_path
+610 20 38 18 ellipse_path
stroke
gsave 10 dict begin
-646 134 moveto 57 -0.5 (Classops) alignedtext
+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 569 145 moveto
-578 144 588 144 597 143 curveto
+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 597 141 moveto
-607 142 lineto
-597 145 lineto
+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 683 133 moveto
-694 131 707 129 718 127 curveto
+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 718 125 moveto
-728 125 lineto
-719 129 lineto
+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
-53 241 44 18 ellipse_path
+40 183 40 18 ellipse_path
stroke
gsave 10 dict begin
-53 236 moveto 67 -0.5 (Pretyping) alignedtext
+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
-164 241 29 18 ellipse_path
+146 64 30 18 ellipse_path
stroke
gsave 10 dict begin
-164 236 moveto 37 -0.5 (Cases) alignedtext
+129 59 moveto
+(Cases)
+[9.36 6.24 5.52 6.24 5.52]
+xshow
end grestore
end grestore
% Pretyping -> Cases
-newpath 98 241 moveto
-107 241 116 241 124 241 curveto
+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 239 moveto
-134 241 lineto
-124 244 lineto
+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
-% Coercion
+% Detyping
gsave 10 dict begin
-272 241 41 18 ellipse_path
+969 164 39 18 ellipse_path
stroke
gsave 10 dict begin
-272 236 moveto 61 -0.5 (Coercion) alignedtext
+942 159 moveto
+(Detyping)
+[10.08 6 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
end grestore
end grestore
-% Cases -> Coercion
-newpath 194 241 moveto
-202 241 211 241 220 241 curveto
+% 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 220 239 moveto
-230 241 lineto
-220 244 lineto
+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
-% Pattern
+% Indrec
gsave 10 dict begin
-898 64 35 18 ellipse_path
+251 271 31 18 ellipse_path
stroke
gsave 10 dict begin
-898 59 moveto 49 -0.5 (Pattern) alignedtext
+233 266 moveto
+(Indrec)
+[4.56 6.96 6.96 4.56 6.24 6.24]
+xshow
end grestore
end grestore
-% Pattern -> Rawterm
-newpath 928 74 moveto
-950 81 982 91 1008 100 curveto
+% 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 1008 97 moveto
-1017 103 lineto
-1007 102 lineto
+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
-% Pattern -> Reductionops
-newpath 934 65 moveto
-983 66 1072 69 1134 70 curveto
+% 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 1132 68 moveto
-1142 70 lineto
-1132 73 lineto
+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
-% Indrec
-gsave 10 dict begin
-898 318 32 18 ellipse_path
+% Detyping -> Inductiveops
+newpath 1009 164 moveto
+1022 164 1036 164 1050 164 curveto
stroke
gsave 10 dict begin
-898 313 moveto 43 -0.5 (Indrec) alignedtext
+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 926 308 moveto
-937 304 949 298 960 291 curveto
-973 282 1004 255 1026 234 curveto
+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 1024 232 moveto
-1033 227 lineto
-1028 236 lineto
+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
-% Evarutil
+% Matching
gsave 10 dict begin
-761 287 39 18 ellipse_path
+610 248 40 18 ellipse_path
stroke
gsave 10 dict begin
-761 282 moveto 56 -0.5 (Evarutil) alignedtext
+582 243 moveto
+(Matching)
+[12.48 6.24 3.84 6 6.96 3.84 6.96 6.96]
+xshow
end grestore
end grestore
-% Evarutil -> Pretype_errors
-newpath 798 281 moveto
-809 279 822 277 834 275 curveto
+% 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 834 273 moveto
-844 273 lineto
-835 277 lineto
+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
-% Evarutil -> Indrec
-newpath 796 295 moveto
-815 299 839 304 859 309 curveto
+% 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 859 306 moveto
-868 311 lineto
-858 311 lineto
+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
-395 241 44 18 ellipse_path
+366 67 40 18 ellipse_path
stroke
gsave 10 dict begin
-395 236 moveto 67 -0.5 (Evarconv) alignedtext
+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 -> Typing
-newpath 440 241 moveto
-452 241 465 241 477 241 curveto
+% 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 477 239 moveto
-487 241 lineto
-477 244 lineto
+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 417 225 moveto
-439 210 471 187 494 170 curveto
+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 491 169 moveto
-501 165 lineto
-494 173 lineto
+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
-% Evarconv -> Evarutil
-newpath 427 254 moveto
-442 259 460 264 476 268 curveto
-482 269 636 278 715 284 curveto
+% 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 712 282 moveto
-722 284 lineto
-712 287 lineto
+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
-% Detyping
+% Clenv
gsave 10 dict begin
-898 156 43 18 ellipse_path
+146 118 30 18 ellipse_path
stroke
gsave 10 dict begin
-898 151 moveto 64 -0.5 (Detyping) alignedtext
+129 113 moveto
+(Clenv)
+[9.36 3.84 6.24 6.48 6.96]
+xshow
end grestore
end grestore
-% Detyping -> Rawterm
-newpath 934 146 moveto
-956 141 983 133 1006 127 curveto
+% 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 1005 125 moveto
-1015 124 lineto
-1006 130 lineto
+newpath 554 122 moveto
+564 118 lineto
+554 115 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% Detyping -> Inductiveops
-newpath 931 168 moveto
-952 176 981 185 1004 194 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1004 191 moveto
-1013 197 lineto
-1003 196 lineto
+newpath 554 122 moveto
+564 118 lineto
+554 115 lineto
closepath
-fill
-0.000 0.000 0.000 edgecolor
+stroke
+end grestore
-% Coercion -> Evarconv
-newpath 314 241 moveto
-323 241 331 241 340 241 curveto
+% 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 340 239 moveto
-350 241 lineto
-340 244 lineto
+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
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index bdbf33327..0e78f4226 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 125
+%%BoundingBox: 35 35 577 136
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,240 +230,404 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 125
+%%PageBoundingBox: 36 36 577 136
%%PageOrientation: Portrait
gsave
-35 35 542 90 boxprim clip newpath
+35 35 542 101 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6136 set_scale
+0.6923 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 125] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Tactic_debug
gsave 10 dict begin
-66 126 57 18 ellipse_path
+163 72 51 18 ellipse_path
stroke
gsave 10 dict begin
-66 121 moveto 93 -0.5 (Tactic_debug) alignedtext
+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
-% Tacmach
+% Refiner
gsave 10 dict begin
-217 72 42 18 ellipse_path
+287 72 34 18 ellipse_path
stroke
gsave 10 dict begin
-217 67 moveto 63 -0.5 (Tacmach) alignedtext
+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 -> Tacmach
-newpath 104 112 moveto
-126 104 154 95 176 87 curveto
+% 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 174 85 moveto
-184 84 lineto
-176 90 lineto
+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
-% Refiner
+% Logic
gsave 10 dict begin
-348 45 37 18 ellipse_path
+390 72 30 18 ellipse_path
stroke
gsave 10 dict begin
-348 40 moveto 53 -0.5 (Refiner) alignedtext
+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 255 64 moveto
-270 61 288 57 304 54 curveto
+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 303 52 moveto
-313 52 lineto
-304 57 lineto
+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
-% Logic
+% Redexpr
gsave 10 dict begin
-452 45 30 18 ellipse_path
+287 126 36 18 ellipse_path
stroke
gsave 10 dict begin
-452 40 moveto 38 -0.5 (Logic) alignedtext
+263 121 moveto
+(Redexpr)
+[9.12 6.24 6.96 5.76 6.96 6.96 4.56]
+xshow
end grestore
end grestore
-% Refiner -> Logic
-newpath 386 45 moveto
-395 45 404 45 412 45 curveto
+% 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 412 43 moveto
-422 45 lineto
-412 48 lineto
+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
-569 45 51 18 ellipse_path
+502 72 45 18 ellipse_path
stroke
gsave 10 dict begin
-569 40 moveto 80 -0.5 (Proof_trees) alignedtext
+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 482 45 moveto
-490 45 499 45 508 45 curveto
+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 508 43 moveto
-518 45 lineto
-508 48 lineto
+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
-707 45 50 18 ellipse_path
+628 72 44 18 ellipse_path
stroke
gsave 10 dict begin
-707 40 moveto 79 -0.5 (Proof_type) alignedtext
+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
-833 45 39 18 ellipse_path
+744 72 35 18 ellipse_path
stroke
gsave 10 dict begin
-833 40 moveto 56 -0.5 (Tacexpr) alignedtext
+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 758 45 moveto
-767 45 775 45 784 45 curveto
+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 784 43 moveto
-794 45 lineto
-784 48 lineto
+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 620 45 moveto
-629 45 637 45 646 45 curveto
+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 646 43 moveto
-656 45 lineto
-646 48 lineto
+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
-66 18 31 18 ellipse_path
+38 112 29 18 ellipse_path
stroke
gsave 10 dict begin
-66 13 moveto 41 -0.5 (Pfedit) alignedtext
+21 107 moveto
+(Pfedit)
+[7.68 4.08 6.24 6.96 3.84 3.84]
+xshow
end grestore
end grestore
% Pfedit -> Tacmach
-newpath 93 28 moveto
-115 36 149 48 175 57 curveto
+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 175 54 moveto
-184 60 lineto
-174 59 lineto
+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
-217 18 56 18 ellipse_path
+163 18 49 18 ellipse_path
stroke
gsave 10 dict begin
-217 13 moveto 91 -0.5 (Evar_refiner) alignedtext
+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 98 18 moveto
-113 18 132 18 150 18 curveto
+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 150 16 moveto
-160 18 lineto
-150 21 lineto
+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 265 28 moveto
-278 30 291 33 304 36 curveto
+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 304 33 moveto
-313 38 lineto
-303 38 lineto
+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
-% Clenv
+% Clenvtac
gsave 10 dict begin
-66 72 31 18 ellipse_path
+38 45 38 18 ellipse_path
stroke
gsave 10 dict begin
-66 67 moveto 40 -0.5 (Clenv) alignedtext
+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
-% Clenv -> Tacmach
-newpath 97 72 moveto
-117 72 142 72 164 72 curveto
+% 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 164 70 moveto
-174 72 lineto
-164 75 lineto
+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
-% Clenv -> Evar_refiner
-newpath 93 62 moveto
-114 55 144 44 170 34 curveto
+% 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 169 32 moveto
-179 31 lineto
-170 37 lineto
+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
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 16e85024d..f4de22b7e 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 123
+%%BoundingBox: 35 35 577 165
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,465 +230,757 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 123
+%%PageBoundingBox: 36 36 577 165
%%PageOrientation: Portrait
gsave
-35 35 542 88 boxprim clip newpath
+35 35 542 130 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.4348 set_scale
+0.4696 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 123] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
-% Termdn
+% Extraargs
gsave 10 dict begin
-1091 180 39 18 ellipse_path
+483 110 40 18 ellipse_path
stroke
gsave 10 dict begin
-1091 175 moveto 56 -0.5 (Termdn) alignedtext
+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
-% Dn
+% Setoid_replace
gsave 10 dict begin
-1207 180 27 18 ellipse_path
+615 64 54 18 ellipse_path
stroke
gsave 10 dict begin
-1207 175 moveto 21 -0.5 (Dn) alignedtext
+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
-% Termdn -> Dn
-newpath 1130 180 moveto
-1143 180 1158 180 1171 180 curveto
+% 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 1170 178 moveto
-1180 180 lineto
-1170 183 lineto
+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
-830 86 34 18 ellipse_path
+884 110 33 18 ellipse_path
stroke
gsave 10 dict begin
-830 81 moveto 46 -0.5 (Tactics) alignedtext
+864 105 moveto
+(Tactics)
+[7.44 6.24 6.24 3.84 3.84 6.24 5.52]
+xshow
end grestore
end grestore
-% Hipattern
+% 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
-958 113 44 18 ellipse_path
+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
-958 108 moveto 66 -0.5 (Hipattern) alignedtext
+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
-% Tactics -> Hipattern
-newpath 862 93 moveto
-876 96 894 100 909 103 curveto
+% 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 910 101 moveto
-919 105 lineto
-909 105 lineto
+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
-% Tacticals
+% Hipattern
gsave 10 dict begin
-958 59 40 18 ellipse_path
+998 110 40 18 ellipse_path
stroke
gsave 10 dict begin
-958 54 moveto 58 -0.5 (Tacticals) alignedtext
+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 -> Tacticals
-newpath 862 79 moveto
-877 76 896 72 912 69 curveto
+% 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 912 67 moveto
-922 67 lineto
-913 71 lineto
+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
-% Wcclausenv
+% Tacticals
gsave 10 dict begin
-1091 59 52 18 ellipse_path
+1112 110 38 18 ellipse_path
stroke
gsave 10 dict begin
-1091 54 moveto 83 -0.5 (Wcclausenv) alignedtext
+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
-% Tacticals -> Wcclausenv
-newpath 998 59 moveto
-1008 59 1018 59 1028 59 curveto
+% 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 1028 57 moveto
-1038 59 lineto
-1028 62 lineto
+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
-439 18 43 18 ellipse_path
+170 191 39 18 ellipse_path
stroke
gsave 10 dict begin
-439 13 moveto 65 -0.5 (Tacinterp) alignedtext
+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
-565 72 28 18 ellipse_path
+483 218 27 18 ellipse_path
stroke
gsave 10 dict begin
-565 67 moveto 35 -0.5 (Auto) alignedtext
+468 213 moveto
+(Auto)
+[9.6 6.96 3.84 6.96]
+xshow
end grestore
end grestore
% Tacinterp -> Auto
-newpath 470 31 moveto
-489 39 514 50 533 58 curveto
+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 533 55 moveto
-541 62 lineto
-531 60 lineto
+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
-% Elim
+% Leminv
gsave 10 dict begin
-565 18 27 18 ellipse_path
+281 166 35 18 ellipse_path
stroke
gsave 10 dict begin
-565 13 moveto 33 -0.5 (Elim) alignedtext
+259 161 moveto
+(Leminv)
+[8.4 6.24 10.8 3.84 6.48 6.96]
+xshow
end grestore
end grestore
-% Tacinterp -> Elim
-newpath 483 18 moveto
-498 18 514 18 528 18 curveto
+% 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 527 16 moveto
-537 18 lineto
-527 21 lineto
+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
-688 18 46 18 ellipse_path
+615 164 42 18 ellipse_path
stroke
gsave 10 dict begin
-688 13 moveto 70 -0.5 (Hiddentac) alignedtext
+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 588 62 moveto
-605 54 629 44 648 36 curveto
+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 647 34 moveto
-657 32 lineto
-649 38 lineto
+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
-688 180 30 18 ellipse_path
+615 218 29 18 ellipse_path
stroke
gsave 10 dict begin
-688 175 moveto 39 -0.5 (Dhyp) alignedtext
+599 213 moveto
+(Dhyp)
+[10.08 6.48 6.96 6.96]
+xshow
end grestore
end grestore
% Auto -> Dhyp
-newpath 578 88 moveto
-597 112 630 152 630 153 curveto
-637 158 646 163 653 167 curveto
+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 654 165 moveto
-662 171 lineto
-652 169 lineto
+newpath 576 222 moveto
+586 218 lineto
+576 215 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% Elim -> Hiddentac
-newpath 593 18 moveto
-604 18 618 18 632 18 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 632 16 moveto
-642 18 lineto
-632 21 lineto
+newpath 576 222 moveto
+586 218 lineto
+576 215 lineto
closepath
-fill
-0.000 0.000 0.000 edgecolor
+stroke
+end grestore
-% Setoid_replace
+% Inv
gsave 10 dict begin
-439 72 60 18 ellipse_path
+379 164 27 18 ellipse_path
stroke
gsave 10 dict begin
-439 67 moveto 99 -0.5 (Setoid_replace) alignedtext
+369 159 moveto
+(Inv)
+[4.56 6.48 6.96]
+xshow
end grestore
end grestore
-% Setoid_replace -> Auto
-newpath 500 72 moveto
-509 72 518 72 527 72 curveto
+% 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 526 70 moveto
-536 72 lineto
-526 75 lineto
+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
-688 126 34 18 ellipse_path
+758 110 32 18 ellipse_path
stroke
gsave 10 dict begin
-688 121 moveto 47 -0.5 (Refine) alignedtext
+739 105 moveto
+(Refine)
+[9.12 6.24 4.8 3.84 6.96 6.24]
+xshow
end grestore
end grestore
% Refine -> Tactics
-newpath 718 117 moveto
-739 112 768 103 791 97 curveto
+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 790 95 moveto
-800 95 lineto
-791 100 lineto
+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
-830 180 47 18 ellipse_path
+758 256 42 18 ellipse_path
stroke
gsave 10 dict begin
-830 175 moveto 73 -0.5 (Nbtermdn) alignedtext
+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
-958 180 42 18 ellipse_path
+884 256 38 18 ellipse_path
stroke
gsave 10 dict begin
-958 175 moveto 62 -0.5 (Btermdn) alignedtext
+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 878 180 moveto
-887 180 897 180 906 180 curveto
+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 906 178 moveto
-916 180 lineto
-906 183 lineto
+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 1000 180 moveto
-1014 180 1029 180 1042 180 curveto
+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 1042 178 moveto
-1052 180 lineto
-1042 183 lineto
+newpath 953 260 moveto
+963 256 lineto
+953 253 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% Leminv
-gsave 10 dict begin
-46 72 38 18 ellipse_path
+newpath 953 260 moveto
+963 256 lineto
+953 253 lineto
+closepath
stroke
-gsave 10 dict begin
-46 67 moveto 54 -0.5 (Leminv) alignedtext
-end grestore
end grestore
-% Inv
+% Elim
gsave 10 dict begin
-173 72 27 18 ellipse_path
+483 164 27 18 ellipse_path
stroke
gsave 10 dict begin
-173 67 moveto 23 -0.5 (Inv) alignedtext
+468 159 moveto
+(Elim)
+[8.4 3.84 3.84 10.8]
+xshow
end grestore
end grestore
-% Leminv -> Inv
-newpath 84 72 moveto
-101 72 120 72 137 72 curveto
+% 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 136 70 moveto
-146 72 lineto
-136 75 lineto
+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
-302 45 40 18 ellipse_path
+483 56 37 18 ellipse_path
stroke
gsave 10 dict begin
-302 40 moveto 58 -0.5 (Equality) alignedtext
+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 199 67 moveto
-215 64 236 59 255 55 curveto
+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 255 53 moveto
-265 53 lineto
-256 57 lineto
+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
-% Equality -> Tacinterp
-newpath 339 38 moveto
-355 35 374 31 391 28 curveto
+% 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 390 26 moveto
-400 26 lineto
-391 31 lineto
+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 339 52 moveto
-352 55 367 58 382 61 curveto
+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 379 58 moveto
-389 62 lineto
-379 63 lineto
+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
-% Hiddentac -> Tactics
-newpath 718 32 moveto
-732 39 746 45 746 45 curveto
-751 48 776 60 798 71 curveto
+% 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 797 68 moveto
-805 74 lineto
-795 72 lineto
+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 713 170 moveto
-724 165 736 159 746 153 curveto
-768 139 790 121 807 107 curveto
+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 804 106 moveto
-813 102 lineto
-807 110 lineto
+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 719 180 moveto
-735 180 755 180 772 180 curveto
+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 772 178 moveto
-782 180 lineto
-772 183 lineto
+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
-688 72 57 18 ellipse_path
+758 18 51 18 ellipse_path
stroke
gsave 10 dict begin
-688 67 moveto 93 -0.5 (Contradiction) alignedtext
+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 743 77 moveto
-758 79 773 80 787 81 curveto
+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 786 78 moveto
-796 82 lineto
-786 83 lineto
+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
-173 18 53 18 ellipse_path
+47 191 47 18 ellipse_path
stroke
gsave 10 dict begin
-173 13 moveto 84 -0.5 (Autorewrite) alignedtext
+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 -> Equality
-newpath 218 28 moveto
-231 30 244 33 256 35 curveto
+% 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 256 32 moveto
-265 37 lineto
-255 37 lineto
+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
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index 216b70bd5..e0355aac0 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002)
-%%For: (filliatr) Jean-Christophe Filliatre
+%%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 180
+%%BoundingBox: 35 35 577 166
%%EndComments
save
%%BeginProlog
@@ -91,7 +91,7 @@ EncodingVector
cleartomark
} bind def
-%%BeginResource: procset
+%%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
@@ -103,7 +103,7 @@ cleartomark
} bind def
% styles
-/solid { } bind def
+/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
@@ -176,6 +176,7 @@ cleartomark
} bind def
/endpage { showpage } bind def
+/showpage { } def
/layercolorseq
[ % layer color sequence - darkest to lightest
@@ -187,8 +188,10 @@ cleartomark
]
def
+/layerlen layercolorseq length def
+
/setlayer {/maxlayer exch def /curlayer exch def
- layercolorseq curlayer get
+ layercolorseq curlayer 1 sub layerlen mod get
aload pop sethsbcolor
/nodecolor {nopcolor} def
/edgecolor {nopcolor} def
@@ -227,491 +230,737 @@ def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 180
+%%PageBoundingBox: 36 36 577 166
%%PageOrientation: Portrait
gsave
-35 35 542 145 boxprim clip newpath
+35 35 542 131 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.4180 set_scale
0 0 translate 0 rotate
-[ /CropBox [36 36 577 180] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
-% Vernacinterp
+% Vernac
gsave 10 dict begin
-947 135 56 18 ellipse_path
+562 145 33 18 ellipse_path
stroke
gsave 10 dict begin
-947 130 moveto 91 -0.5 (Vernacinterp) alignedtext
+541 140 moveto
+(Vernac)
+[8.88 6.24 4.8 6.96 6.24 6.24]
+xshow
end grestore
end grestore
-% Himsg
+% Vernacentries
gsave 10 dict begin
-1092 60 33 18 ellipse_path
+724 158 52 18 ellipse_path
stroke
gsave 10 dict begin
-1092 55 moveto 45 -0.5 (Himsg) alignedtext
+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
-% Vernacinterp -> Himsg
-newpath 979 120 moveto
-991 114 1003 109 1004 108 curveto
-1015 103 1042 88 1063 76 curveto
+% 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 1059 75 moveto
-1069 73 lineto
-1061 80 lineto
+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
-% Vernacexpr
+% Vernacinterp
gsave 10 dict begin
-1232 179 51 18 ellipse_path
+862 158 50 18 ellipse_path
stroke
gsave 10 dict begin
-1232 174 moveto 81 -0.5 (Vernacexpr) alignedtext
+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
-% Vernacinterp -> Vernacexpr
-newpath 1002 139 moveto
-1056 143 1131 149 1144 152 curveto
-1159 154 1173 159 1187 163 curveto
+% 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 1187 160 moveto
-1196 166 lineto
-1186 165 lineto
+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
-% Vernacentries
+% Discharge
gsave 10 dict begin
-795 158 58 18 ellipse_path
+862 212 42 18 ellipse_path
stroke
gsave 10 dict begin
-795 153 moveto 95 -0.5 (Vernacentries) alignedtext
+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 -> Vernacinterp
-newpath 848 150 moveto
-860 148 873 146 886 144 curveto
+% 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 886 142 moveto
-896 143 lineto
-886 146 lineto
+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
-% Discharge
+% Mltop
gsave 10 dict begin
-947 287 45 18 ellipse_path
+862 104 31 18 ellipse_path
stroke
gsave 10 dict begin
-947 282 moveto 68 -0.5 (Discharge) alignedtext
+844 99 moveto
+(Mltop)
+[12.48 3.84 3.84 6.96 6.96]
+xshow
end grestore
end grestore
-% Vernacentries -> Discharge
-newpath 809 176 moveto
-826 197 857 233 890 258 curveto
-895 262 902 266 908 269 curveto
+% 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 909 267 moveto
-917 273 lineto
-907 271 lineto
+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
-% Metasyntax
+% Record
gsave 10 dict begin
-1092 179 51 18 ellipse_path
+862 281 33 18 ellipse_path
stroke
gsave 10 dict begin
-1092 174 moveto 81 -0.5 (Metasyntax) alignedtext
+842 276 moveto
+(Record)
+[9.12 6.24 6.24 6.96 4.32 6.96]
+xshow
end grestore
end grestore
-% Vernacentries -> Metasyntax
-newpath 852 162 moveto
-903 166 978 171 1030 174 curveto
+% 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 1031 172 moveto
-1041 175 lineto
-1031 177 lineto
+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
-% Mltop
+% Himsg
gsave 10 dict begin
-947 81 32 18 ellipse_path
+991 85 32 18 ellipse_path
stroke
gsave 10 dict begin
-947 76 moveto 42 -0.5 (Mltop) alignedtext
+971 80 moveto
+(Himsg)
+[10.08 3.84 10.8 5.52 6.96]
+xshow
end grestore
end grestore
-% Vernacentries -> Mltop
-newpath 825 142 moveto
-848 130 878 114 890 108 curveto
-895 106 905 101 915 96 curveto
+% 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 912 95 moveto
-922 93 lineto
-914 99 lineto
+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
-% Record
+% Vernacexpr
gsave 10 dict begin
-947 231 35 18 ellipse_path
+1246 221 45 18 ellipse_path
stroke
gsave 10 dict begin
-947 226 moveto 49 -0.5 (Record) alignedtext
+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
-% Vernacentries -> Record
-newpath 827 173 moveto
-851 186 886 202 913 214 curveto
+% 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 913 211 moveto
-921 218 lineto
-911 216 lineto
+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
-1232 283 28 18 ellipse_path
+1117 238 28 18 ellipse_path
stroke
gsave 10 dict begin
-1232 278 moveto 34 -0.5 (Class) alignedtext
+1101 233 moveto
+(Class)
+[9.36 3.84 6.24 5.52 5.52]
+xshow
end grestore
end grestore
% Discharge -> Class
-newpath 983 298 moveto
-1004 305 1029 312 1040 314 curveto
-1086 320 1099 321 1144 314 curveto
-1155 312 1179 304 1198 296 curveto
+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 1198 293 moveto
-1208 292 lineto
-1200 298 lineto
+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
-1092 287 47 18 ellipse_path
+991 196 42 18 ellipse_path
stroke
gsave 10 dict begin
-1092 282 moveto 72 -0.5 (Recordobj) alignedtext
+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 992 287 moveto
-1006 287 1021 287 1035 287 curveto
+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 1035 285 moveto
-1045 287 lineto
-1035 290 lineto
+newpath 940 205 moveto
+950 201 lineto
+940 199 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% Metasyntax -> Vernacexpr
-newpath 1144 179 moveto
-1153 179 1161 179 1170 179 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 1170 177 moveto
-1180 179 lineto
-1170 182 lineto
+newpath 940 205 moveto
+950 201 lineto
+940 199 lineto
closepath
-fill
-0.000 0.000 0.000 edgecolor
+stroke
+end grestore
% Command
gsave 10 dict begin
-1092 233 47 18 ellipse_path
+991 288 42 18 ellipse_path
stroke
gsave 10 dict begin
-1092 228 moveto 73 -0.5 (Command) alignedtext
+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 983 231 moveto
-999 231 1017 232 1034 232 curveto
+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 1034 230 moveto
-1044 232 lineto
-1034 235 lineto
+newpath 938 288 moveto
+948 286 lineto
+938 282 lineto
closepath
fill
0.000 0.000 0.000 edgecolor
-
-% Vernac
-gsave 10 dict begin
-614 145 36 18 ellipse_path
+newpath 938 288 moveto
+948 286 lineto
+938 282 lineto
+closepath
stroke
-gsave 10 dict begin
-614 140 moveto 50 -0.5 (Vernac) alignedtext
-end grestore
end grestore
-% Vernac -> Vernacentries
-newpath 650 148 moveto
-672 149 701 151 728 153 curveto
-stroke
-0.000 0.000 0.000 edgecolor
-newpath 728 151 moveto
-738 154 lineto
-728 155 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-
% Toplevel
gsave 10 dict begin
-275 72 40 18 ellipse_path
+255 72 37 18 ellipse_path
stroke
gsave 10 dict begin
-275 67 moveto 59 -0.5 (Toplevel) alignedtext
+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
-422 72 69 18 ellipse_path
+390 72 61 18 ellipse_path
stroke
gsave 10 dict begin
-422 67 moveto 117 -0.5 (Protectedtoplevel) alignedtext
+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 316 72 moveto
-324 72 333 72 342 72 curveto
+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 342 70 moveto
-352 72 lineto
-342 75 lineto
+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 461 87 moveto
-496 100 545 118 578 131 curveto
+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 577 128 moveto
-585 134 lineto
-575 132 lineto
+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
-795 42 36 18 ellipse_path
+724 65 34 18 ellipse_path
stroke
gsave 10 dict begin
-795 37 moveto 51 -0.5 (Cerrors) alignedtext
+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 490 68 moveto
-547 65 629 60 700 53 curveto
-717 52 735 50 751 48 curveto
+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 750 46 moveto
-760 47 lineto
-750 51 lineto
+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
-614 26 85 18 ellipse_path
+562 26 73 18 ellipse_path
stroke
gsave 10 dict begin
-614 21 moveto 149 -0.5 (Line_oriented_parser) alignedtext
+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 473 60 moveto
-496 55 524 48 548 42 curveto
+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 547 40 moveto
-557 40 lineto
-548 45 lineto
+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 -> Vernacexpr
-newpath 1126 220 moveto
-1144 213 1168 204 1188 196 curveto
+% 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 1187 194 moveto
-1197 192 lineto
-1189 198 lineto
+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 1127 245 moveto
-1149 253 1177 263 1199 271 curveto
+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 1199 268 moveto
-1207 274 lineto
-1197 273 lineto
+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 832 44 moveto
-882 47 972 53 1004 54 curveto
-1019 55 1035 56 1049 57 curveto
+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 1049 55 moveto
-1059 58 lineto
-1049 59 lineto
+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
-48 126 39 18 ellipse_path
+38 126 37 18 ellipse_path
stroke
gsave 10 dict begin
-48 121 moveto 57 -0.5 (Minicoq) alignedtext
+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
-161 126 36 18 ellipse_path
+147 126 34 18 ellipse_path
stroke
gsave 10 dict begin
-161 121 moveto 51 -0.5 (Fhimsg) alignedtext
+125 121 moveto
+(Fhimsg)
+[7.68 6.96 3.84 10.8 5.52 6.96]
+xshow
end grestore
end grestore
% Minicoq -> Fhimsg
-newpath 88 126 moveto
-97 126 106 126 114 126 curveto
+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 114 124 moveto
-124 126 lineto
-114 129 lineto
+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
-48 45 36 18 ellipse_path
+38 45 34 18 ellipse_path
stroke
gsave 10 dict begin
-48 40 moveto 50 -0.5 (Coqtop) alignedtext
+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
-161 72 36 18 ellipse_path
+147 72 34 18 ellipse_path
stroke
gsave 10 dict begin
-161 67 moveto 50 -0.5 (Coqinit) alignedtext
+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 81 53 moveto
-93 56 106 59 118 62 curveto
+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 119 60 moveto
-128 64 lineto
-118 64 lineto
+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
-161 18 32 18 ellipse_path
+147 18 31 18 ellipse_path
stroke
gsave 10 dict begin
-161 13 moveto 42 -0.5 (Usage) alignedtext
+129 13 moveto
+(Usage)
+[10.08 5.52 6.24 6.72 6.24]
+xshow
end grestore
end grestore
% Coqtop -> Usage
-newpath 81 37 moveto
-94 34 109 31 122 27 curveto
+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 121 25 moveto
-131 25 lineto
-122 30 lineto
+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 197 72 moveto
-206 72 215 72 224 72 curveto
+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 224 70 moveto
-234 72 lineto
-224 75 lineto
+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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 05:39:33 +0000