Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 1259 insertions, 0 deletions

diff --git a/dev/doc/pretyping.dep.ps b/dev/doc/pretyping.dep.ps
new file mode 100644
index 00000000..02d1b8b5
--- /dev/null
+++ b/dev/doc/pretyping.dep.ps
@@ -0,0 +1,1259 @@
+%!PS-Adobe-2.0
+%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005)
+%%For: (herbelin) Hugo Herbelin
+%%Title: G
+%%Pages: (atend)
+%%BoundingBox: 35 35 577 146
+%%EndComments
+save
+%%BeginProlog
+/DotDict 200 dict def
+DotDict begin
+
+/setupLatin1 {
+mark
+/EncodingVector 256 array def
+ EncodingVector 0
+
+ISOLatin1Encoding 0 255 getinterval putinterval
+
+EncodingVector
+  dup 306 /AE
+  dup 301 /Aacute
+  dup 302 /Acircumflex
+  dup 304 /Adieresis
+  dup 300 /Agrave
+  dup 305 /Aring
+  dup 303 /Atilde
+  dup 307 /Ccedilla
+  dup 311 /Eacute
+  dup 312 /Ecircumflex
+  dup 313 /Edieresis
+  dup 310 /Egrave
+  dup 315 /Iacute
+  dup 316 /Icircumflex
+  dup 317 /Idieresis
+  dup 314 /Igrave
+  dup 334 /Udieresis
+  dup 335 /Yacute
+  dup 376 /thorn
+  dup 337 /germandbls
+  dup 341 /aacute
+  dup 342 /acircumflex
+  dup 344 /adieresis
+  dup 346 /ae
+  dup 340 /agrave
+  dup 345 /aring
+  dup 347 /ccedilla
+  dup 351 /eacute
+  dup 352 /ecircumflex
+  dup 353 /edieresis
+  dup 350 /egrave
+  dup 355 /iacute
+  dup 356 /icircumflex
+  dup 357 /idieresis
+  dup 354 /igrave
+  dup 360 /dcroat
+  dup 361 /ntilde
+  dup 363 /oacute
+  dup 364 /ocircumflex
+  dup 366 /odieresis
+  dup 362 /ograve
+  dup 365 /otilde
+  dup 370 /oslash
+  dup 372 /uacute
+  dup 373 /ucircumflex
+  dup 374 /udieresis
+  dup 371 /ugrave
+  dup 375 /yacute
+  dup 377 /ydieresis  
+
+% Set up ISO Latin 1 character encoding
+/starnetISO {
+        dup dup findfont dup length dict begin
+        { 1 index /FID ne { def }{ pop pop } ifelse
+        } forall
+        /Encoding EncodingVector def
+        currentdict end definefont
+} def
+/Times-Roman starnetISO def
+/Times-Italic starnetISO def
+/Times-Bold starnetISO def
+/Times-BoldItalic starnetISO def
+/Helvetica starnetISO def
+/Helvetica-Oblique starnetISO def
+/Helvetica-Bold starnetISO def
+/Helvetica-BoldOblique starnetISO def
+/Courier starnetISO def
+/Courier-Oblique starnetISO def
+/Courier-Bold starnetISO def
+/Courier-BoldOblique starnetISO def
+cleartomark
+} bind def
+
+%%BeginResource: procset graphviz 0 0
+/coord-font-family /Times-Roman def
+/default-font-family /Times-Roman def
+/coordfont coord-font-family findfont 8 scalefont def
+
+/InvScaleFactor 1.0 def
+/set_scale {
+	dup 1 exch div /InvScaleFactor exch def
+	dup scale
+} bind def
+
+% styles
+/solid { [] 0 setdash } bind def
+/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
+/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
+/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
+/bold { 2 setlinewidth } bind def
+/filled { } bind def
+/unfilled { } bind def
+/rounded { } bind def
+/diagonals { } bind def
+
+% hooks for setting color 
+/nodecolor { sethsbcolor } bind def
+/edgecolor { sethsbcolor } bind def
+/graphcolor { sethsbcolor } bind def
+/nopcolor {pop pop pop} bind def
+
+/beginpage {	% i j npages
+	/npages exch def
+	/j exch def
+	/i exch def
+	/str 10 string def
+	npages 1 gt {
+		gsave
+			coordfont setfont
+			0 0 moveto
+			(\() show i str cvs show (,) show j str cvs show (\)) show
+		grestore
+	} if
+} bind def
+
+/set_font {
+	findfont exch
+	scalefont setfont
+} def
+
+% draw aligned label in bounding box aligned to current point
+/alignedtext {			% width adj text
+	/text exch def
+	/adj exch def
+	/width exch def
+	gsave
+		width 0 gt {
+			text stringwidth pop adj mul 0 rmoveto
+		} if
+		[] 0 setdash
+		text show
+	grestore
+} def
+
+/boxprim {				% xcorner ycorner xsize ysize
+		4 2 roll
+		moveto
+		2 copy
+		exch 0 rlineto
+		0 exch rlineto
+		pop neg 0 rlineto
+		closepath
+} bind def
+
+/ellipse_path {
+	/ry exch def
+	/rx exch def
+	/y exch def
+	/x exch def
+	matrix currentmatrix
+	newpath
+	x y translate
+	rx ry scale
+	0 0 1 0 360 arc
+	setmatrix
+} bind def
+
+/endpage { showpage } bind def
+/showpage { } def
+
+/layercolorseq
+	[	% layer color sequence - darkest to lightest
+		[0 0 0]
+		[.2 .8 .8]
+		[.4 .8 .8]
+		[.6 .8 .8]
+		[.8 .8 .8]
+	]
+def
+
+/layerlen layercolorseq length def
+
+/setlayer {/maxlayer exch def /curlayer exch def
+	layercolorseq curlayer 1 sub layerlen mod get
+	aload pop sethsbcolor
+	/nodecolor {nopcolor} def
+	/edgecolor {nopcolor} def
+	/graphcolor {nopcolor} def
+} bind def
+
+/onlayer { curlayer ne {invis} if } def
+
+/onlayers {
+	/myupper exch def
+	/mylower exch def
+	curlayer mylower lt
+	curlayer myupper gt
+	or
+	{invis} if
+} def
+
+/curlayer 0 def
+
+%%EndResource
+%%EndProlog
+%%BeginSetup
+14 default-font-family set_font
+1 setmiterlimit
+% /arrowlength 10 def
+% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+    userdict (<<) cvn ([) cvn load put
+    userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndSetup
+%%Page: 1 1
+%%PageBoundingBox: 36 36 577 146
+%%PageOrientation: Portrait
+gsave
+35 35 542 111 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0.3600 set_scale
+0 0 translate 0 rotate
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+%	Unification
+gsave 10 dict begin
+610 118 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+577 113 moveto
+(Unification)
+[9.6 6.96 3.84 4.8 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Evarutil
+gsave 10 dict begin
+728 72 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+705 67 moveto
+(Evarutil)
+[8.4 6.72 6.24 4.8 6.96 3.84 3.84 3.84]
+xshow
+end grestore
+end grestore
+
+%	Unification -> Evarutil
+newpath 643 105 moveto
+657 99 674 93 689 87 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 691 90 moveto
+699 83 lineto
+688 83 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 691 90 moveto
+699 83 lineto
+688 83 lineto
+closepath
+stroke
+end grestore
+
+%	Pattern
+gsave 10 dict begin
+728 210 33 18 ellipse_path
+stroke
+gsave 10 dict begin
+708 205 moveto
+(Pattern)
+[7.44 6.24 3.84 3.84 6.24 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+%	Unification -> Pattern
+newpath 631 134 moveto
+650 150 680 173 701 189 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 699 192 moveto
+709 195 lineto
+703 186 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 699 192 moveto
+709 195 lineto
+703 186 lineto
+closepath
+stroke
+end grestore
+
+%	Retyping
+gsave 10 dict begin
+839 118 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+813 113 moveto
+(Retyping)
+[9.12 6 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Unification -> Retyping
+newpath 656 118 moveto
+695 118 750 118 790 118 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 790 122 moveto
+800 118 lineto
+790 115 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 790 122 moveto
+800 118 lineto
+790 115 lineto
+closepath
+stroke
+end grestore
+
+%	Typing
+gsave 10 dict begin
+839 64 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+819 59 moveto
+(Typing)
+[6.96 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Evarutil -> Typing
+newpath 764 69 moveto
+775 68 786 67 797 67 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 797 70 moveto
+807 66 lineto
+797 64 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 797 70 moveto
+807 66 lineto
+797 64 lineto
+closepath
+stroke
+end grestore
+
+%	Rawterm
+gsave 10 dict begin
+1109 110 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+1083 105 moveto
+(Rawterm)
+[9.36 5.76 10.08 3.84 6.24 4.8 10.8]
+xshow
+end grestore
+end grestore
+
+%	Pattern -> Rawterm
+newpath 759 216 moveto
+816 226 939 239 1024 191 curveto
+1049 176 1038 155 1060 138 curveto
+1069 131 1077 130 1084 129 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1085 132 moveto
+1094 127 lineto
+1084 126 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1085 132 moveto
+1094 127 lineto
+1084 126 lineto
+closepath
+stroke
+end grestore
+
+%	Inductiveops
+gsave 10 dict begin
+1109 164 49 18 ellipse_path
+stroke
+gsave 10 dict begin
+1073 159 moveto
+(Inductiveops)
+[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	Retyping -> Inductiveops
+newpath 878 120 moveto
+915 122 974 126 1024 137 curveto
+1037 139 1051 144 1064 148 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1063 151 moveto
+1074 151 lineto
+1065 145 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1063 151 moveto
+1074 151 lineto
+1065 145 lineto
+closepath
+stroke
+end grestore
+
+%	Pretype_errors
+gsave 10 dict begin
+969 72 54 18 ellipse_path
+stroke
+gsave 10 dict begin
+927 67 moveto
+(Pretype_errors)
+[7.68 4.56 6 3.84 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52]
+xshow
+end grestore
+end grestore
+
+%	Typing -> Pretype_errors
+newpath 871 66 moveto
+881 67 893 68 905 68 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 905 71 moveto
+915 69 lineto
+905 65 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 905 71 moveto
+915 69 lineto
+905 65 lineto
+closepath
+stroke
+end grestore
+
+%	Pretype_errors -> Inductiveops
+newpath 998 87 moveto
+1007 92 1016 98 1024 104 curveto
+1042 116 1043 124 1060 137 curveto
+1063 139 1067 142 1071 144 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1070 147 moveto
+1080 149 lineto
+1073 141 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1070 147 moveto
+1080 149 lineto
+1073 141 lineto
+closepath
+stroke
+end grestore
+
+%	Pretype_errors -> Rawterm
+newpath 1011 84 moveto
+1029 88 1048 94 1065 98 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1064 101 moveto
+1075 101 lineto
+1066 95 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1064 101 moveto
+1075 101 lineto
+1066 95 lineto
+closepath
+stroke
+end grestore
+
+%	Tacred
+gsave 10 dict begin
+728 18 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+709 13 moveto
+(Tacred)
+[7.44 6.24 6.24 4.56 6.24 6.96]
+xshow
+end grestore
+end grestore
+
+%	Tacred -> Retyping
+newpath 748 32 moveto
+754 36 759 41 764 45 curveto
+783 63 782 73 800 91 curveto
+802 93 805 95 808 97 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 806 100 moveto
+816 103 lineto
+810 94 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 806 100 moveto
+816 103 lineto
+810 94 lineto
+closepath
+stroke
+end grestore
+
+%	Tacred -> Typing
+newpath 754 29 moveto
+769 35 787 43 803 49 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 802 53 moveto
+813 53 lineto
+805 46 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 802 53 moveto
+813 53 lineto
+805 46 lineto
+closepath
+stroke
+end grestore
+
+%	Cbv
+gsave 10 dict begin
+1246 41 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+1234 36 moveto
+(Cbv)
+[9.36 6.48 6.96]
+xshow
+end grestore
+end grestore
+
+%	Tacred -> Cbv
+newpath 760 19 moveto
+852 23 1111 35 1209 40 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1209 44 moveto
+1219 40 lineto
+1209 37 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1209 44 moveto
+1219 40 lineto
+1209 37 lineto
+closepath
+stroke
+end grestore
+
+%	Evd
+gsave 10 dict begin
+1361 110 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+1349 105 moveto
+(Evd)
+[8.4 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Cbv -> Evd
+newpath 1266 53 moveto
+1284 64 1312 80 1332 93 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1331 96 moveto
+1341 98 lineto
+1334 90 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1331 96 moveto
+1341 98 lineto
+1334 90 lineto
+closepath
+stroke
+end grestore
+
+%	Reductionops
+gsave 10 dict begin
+1246 164 51 18 ellipse_path
+stroke
+gsave 10 dict begin
+1207 159 moveto
+(Reductionops)
+[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	Inductiveops -> Reductionops
+newpath 1158 164 moveto
+1167 164 1175 164 1184 164 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1184 168 moveto
+1194 164 lineto
+1184 161 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1184 168 moveto
+1194 164 lineto
+1184 161 lineto
+closepath
+stroke
+end grestore
+
+%	Reductionops -> Evd
+newpath 1277 150 moveto
+1294 142 1313 133 1330 125 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1331 128 moveto
+1339 121 lineto
+1328 122 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1331 128 moveto
+1339 121 lineto
+1328 122 lineto
+closepath
+stroke
+end grestore
+
+%	Termops
+gsave 10 dict begin
+1462 110 37 18 ellipse_path
+stroke
+gsave 10 dict begin
+1437 105 moveto
+(Termops)
+[7.2 6.24 4.8 10.8 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	Evd -> Termops
+newpath 1388 110 moveto
+1396 110 1405 110 1414 110 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1414 114 moveto
+1424 110 lineto
+1414 107 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1414 114 moveto
+1424 110 lineto
+1414 107 lineto
+closepath
+stroke
+end grestore
+
+%	Recordops
+gsave 10 dict begin
+485 24 43 18 ellipse_path
+stroke
+gsave 10 dict begin
+455 19 moveto
+(Recordops)
+[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	Classops
+gsave 10 dict begin
+610 20 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+584 15 moveto
+(Classops)
+[9.36 3.84 6.24 5.52 5.52 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	Recordops -> Classops
+newpath 528 23 moveto
+538 22 550 22 561 22 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 561 25 moveto
+571 21 lineto
+561 19 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 561 25 moveto
+571 21 lineto
+561 19 lineto
+closepath
+stroke
+end grestore
+
+%	Classops -> Tacred
+newpath 649 19 moveto
+661 19 674 19 686 19 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 686 23 moveto
+696 19 lineto
+686 16 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 686 23 moveto
+696 19 lineto
+686 16 lineto
+closepath
+stroke
+end grestore
+
+%	Rawterm -> Evd
+newpath 1148 110 moveto
+1196 110 1277 110 1324 110 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1324 114 moveto
+1334 110 lineto
+1324 107 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1324 114 moveto
+1334 110 lineto
+1324 107 lineto
+closepath
+stroke
+end grestore
+
+%	Pretyping
+gsave 10 dict begin
+40 183 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+13 178 moveto
+(Pretyping)
+[7.68 4.56 6 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Pretyping -> Pattern
+newpath 78 189 moveto
+121 194 191 202 251 202 curveto
+251 202 251 202 485 202 curveto
+556 202 636 205 685 208 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 685 212 moveto
+695 208 lineto
+685 205 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 685 212 moveto
+695 208 lineto
+685 205 lineto
+closepath
+stroke
+end grestore
+
+%	Cases
+gsave 10 dict begin
+146 64 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+129 59 moveto
+(Cases)
+[9.36 6.24 5.52 6.24 5.52]
+xshow
+end grestore
+end grestore
+
+%	Pretyping -> Cases
+newpath 53 166 moveto
+68 147 93 115 116 91 curveto
+118 89 119 88 121 86 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 124 88 moveto
+129 79 lineto
+119 83 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 124 88 moveto
+129 79 lineto
+119 83 lineto
+closepath
+stroke
+end grestore
+
+%	Detyping
+gsave 10 dict begin
+969 164 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+942 159 moveto
+(Detyping)
+[10.08 6 3.84 6.96 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Pretyping -> Detyping
+newpath 78 177 moveto
+121 172 191 164 251 164 curveto
+251 164 251 164 728 164 curveto
+794 164 870 164 919 164 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 919 168 moveto
+929 164 lineto
+919 161 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 919 168 moveto
+929 164 lineto
+919 161 lineto
+closepath
+stroke
+end grestore
+
+%	Indrec
+gsave 10 dict begin
+251 271 31 18 ellipse_path
+stroke
+gsave 10 dict begin
+233 266 moveto
+(Indrec)
+[4.56 6.96 6.96 4.56 6.24 6.24]
+xshow
+end grestore
+end grestore
+
+%	Pretyping -> Indrec
+newpath 69 195 moveto
+83 202 101 209 116 216 curveto
+150 230 188 246 216 257 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 214 260 moveto
+225 261 lineto
+217 254 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 214 260 moveto
+225 261 lineto
+217 254 lineto
+closepath
+stroke
+end grestore
+
+%	Coercion
+gsave 10 dict begin
+251 67 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+225 62 moveto
+(Coercion)
+[9.36 6.96 6.24 4.56 6.24 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Cases -> Coercion
+newpath 176 65 moveto
+184 65 193 66 202 66 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 202 70 moveto
+212 66 lineto
+202 63 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 202 70 moveto
+212 66 lineto
+202 63 lineto
+closepath
+stroke
+end grestore
+
+%	Detyping -> Inductiveops
+newpath 1009 164 moveto
+1022 164 1036 164 1050 164 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1050 168 moveto
+1060 164 lineto
+1050 161 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1050 168 moveto
+1060 164 lineto
+1050 161 lineto
+closepath
+stroke
+end grestore
+
+%	Detyping -> Rawterm
+newpath 999 152 moveto
+1020 144 1047 133 1069 125 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1070 128 moveto
+1079 122 lineto
+1068 122 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1070 128 moveto
+1079 122 lineto
+1068 122 lineto
+closepath
+stroke
+end grestore
+
+%	Indrec -> Inductiveops
+newpath 281 276 moveto
+325 283 412 294 485 294 curveto
+485 294 485 294 839 294 curveto
+937 294 1036 225 1082 188 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1085 190 moveto
+1090 181 lineto
+1080 185 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1085 190 moveto
+1090 181 lineto
+1080 185 lineto
+closepath
+stroke
+end grestore
+
+%	Matching
+gsave 10 dict begin
+610 248 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+582 243 moveto
+(Matching)
+[12.48 6.24 3.84 6 6.96 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	Matching -> Pattern
+newpath 643 237 moveto
+658 232 675 227 689 222 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 690 225 moveto
+699 219 lineto
+688 219 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 690 225 moveto
+699 219 lineto
+688 219 lineto
+closepath
+stroke
+end grestore
+
+%	Matching -> Reductionops
+newpath 650 250 moveto
+696 253 773 256 839 256 curveto
+839 256 839 256 969 256 curveto
+1059 256 1159 212 1210 184 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 1212 187 moveto
+1219 179 lineto
+1209 181 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 1212 187 moveto
+1219 179 lineto
+1209 181 lineto
+closepath
+stroke
+end grestore
+
+%	Evarconv
+gsave 10 dict begin
+366 67 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+339 62 moveto
+(Evarconv)
+[8.4 6.72 6.24 4.56 6.24 6.96 6.48 6.96]
+xshow
+end grestore
+end grestore
+
+%	Evarconv -> Evarutil
+newpath 406 68 moveto
+474 69 610 71 682 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 682 76 moveto
+692 72 lineto
+682 69 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 682 76 moveto
+692 72 lineto
+682 69 lineto
+closepath
+stroke
+end grestore
+
+%	Evarconv -> Recordops
+newpath 397 56 moveto
+411 51 428 45 442 39 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 443 42 moveto
+452 36 lineto
+441 36 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 443 42 moveto
+452 36 lineto
+441 36 lineto
+closepath
+stroke
+end grestore
+
+%	Coercion -> Evarconv
+newpath 290 67 moveto
+299 67 307 67 316 67 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 316 71 moveto
+326 67 lineto
+316 64 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 316 71 moveto
+326 67 lineto
+316 64 lineto
+closepath
+stroke
+end grestore
+
+%	Clenv
+gsave 10 dict begin
+146 118 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+129 113 moveto
+(Clenv)
+[9.36 3.84 6.24 6.48 6.96]
+xshow
+end grestore
+end grestore
+
+%	Clenv -> Unification
+newpath 176 118 moveto
+252 118 455 118 554 118 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 554 122 moveto
+564 118 lineto
+554 115 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 554 122 moveto
+564 118 lineto
+554 115 lineto
+closepath
+stroke
+end grestore
+
+%	Clenv -> Coercion
+newpath 170 107 moveto
+183 100 200 93 215 85 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 217 88 moveto
+224 80 lineto
+214 82 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 217 88 moveto
+224 80 lineto
+214 82 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF