MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6623 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 914 insertions, 206 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index a0be6b4ca5..3c00121e81 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