MAJ

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

1 files changed, 728 insertions, 237 deletions

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