From 44e7cd6dd3d4f50391c20bd27176fff30e1da33c Mon Sep 17 00:00:00 2001 From: coq Date: Thu, 14 Sep 2000 13:22:58 +0000 Subject: Minor correction for Ocamlweb + doc update git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@608 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/kernel.dep.ps | 351 +++++++++++++++++++------------------------------ doc/library.dep.ps | 245 ++++++++++++++++------------------- doc/parsing.dep.ps | 299 +++++++++++++++++++++++------------------- doc/pretyping.dep.ps | 319 +++++++++++++++++++++++++-------------------- doc/proofs.dep.ps | 31 ++++- doc/tactics.dep.ps | 359 ++++++++++++++++++++++++++++++++++----------------- doc/toplevel.dep.ps | 304 +++++++++++++++++++++---------------------- 7 files changed, 1001 insertions(+), 907 deletions(-) (limited to 'doc') diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps index 8a9253ae9..7b6640611 100644 --- a/doc/kernel.dep.ps +++ b/doc/kernel.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 577 94 +%%BoundingBox: 36 36 577 70 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,385 +139,298 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 577 94 +%%PageBoundingBox: 36 36 577 70 gsave -35 35 542 59 boxprim clip newpath +35 35 542 35 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.4000 set_scale +0.3745 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Univ gsave 10 dict begin -1221 72 27 18 ellipse_path +1319 45 27 18 ellipse_path stroke gsave 10 dict begin -1221 73 moveto (Univ) 28 14.00 -0.50 alignedtext +1319 46 moveto (Univ) 28 14.00 -0.50 alignedtext end grestore end grestore % Names gsave 10 dict begin -1320 45 29 18 ellipse_path +1412 45 29 18 ellipse_path stroke gsave 10 dict begin -1320 46 moveto (Names) 38 14.00 -0.50 alignedtext +1412 46 moveto (Names) 38 14.00 -0.50 alignedtext end grestore end grestore % Univ -> Names -newpath 1246 65 moveto -1258 62 1271 58 1284 55 curveto +newpath 1346 45 moveto +1354 45 1363 45 1372 45 curveto stroke -newpath 1283 53 moveto -1293 52 lineto -1284 58 lineto +newpath 1372 43 moveto +1382 45 lineto +1372 48 lineto closepath gsave 0 setgray stroke grestore fill % Typeops gsave 10 dict begin -265 70 34 18 ellipse_path +265 45 34 18 ellipse_path stroke gsave 10 dict begin -265 71 moveto (Typeops) 48 14.00 -0.50 alignedtext +265 46 moveto (Typeops) 48 14.00 -0.50 alignedtext end grestore end grestore -% Reduction +% Inductive gsave 10 dict begin -375 97 39 18 ellipse_path +381 72 36 18 ellipse_path stroke gsave 10 dict begin -375 98 moveto (Reduction) 57 14.00 -0.50 alignedtext +381 73 moveto (Inductive) 52 14.00 -0.50 alignedtext end grestore end grestore -% Typeops -> Reduction -newpath 296 78 moveto -307 80 319 83 330 86 curveto +% Typeops -> Inductive +newpath 297 52 moveto +310 55 325 58 339 62 curveto stroke -newpath 331 84 moveto -340 89 lineto -330 89 lineto +newpath 339 59 moveto +348 64 lineto +338 64 lineto closepath gsave 0 setgray stroke grestore fill % Type_errors gsave 10 dict begin -495 45 44 18 ellipse_path +381 18 44 18 ellipse_path stroke gsave 10 dict begin -495 46 moveto (Type_errors) 68 14.00 -0.50 alignedtext +381 19 moveto (Type_errors) 68 14.00 -0.50 alignedtext end grestore end grestore % Typeops -> Type_errors -newpath 299 66 moveto -337 62 399 55 443 51 curveto -stroke -newpath 442 49 moveto -452 50 lineto -442 54 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Closure -gsave 10 dict begin -495 99 32 18 ellipse_path -stroke -gsave 10 dict begin -495 100 moveto (Closure) 43 14.00 -0.50 alignedtext -end grestore -end grestore - -% Reduction -> Closure -newpath 414 98 moveto -427 98 441 98 453 98 curveto -stroke -newpath 453 96 moveto -463 98 lineto -453 101 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Environ -gsave 10 dict begin -815 72 33 18 ellipse_path +newpath 297 38 moveto +308 36 321 33 333 30 curveto stroke -gsave 10 dict begin -815 73 moveto (Environ) 45 14.00 -0.50 alignedtext -end grestore -end grestore - -% Type_errors -> Environ -newpath 539 49 moveto -601 54 713 63 774 68 curveto -stroke -newpath 772 65 moveto -782 69 lineto -772 70 lineto +newpath 332 28 moveto +342 27 lineto +333 33 lineto closepath gsave 0 setgray stroke grestore fill -% Inductive +% Reduction gsave 10 dict begin -927 126 36 18 ellipse_path +501 45 39 18 ellipse_path stroke gsave 10 dict begin -927 127 moveto (Inductive) 52 14.00 -0.50 alignedtext +501 46 moveto (Reduction) 57 14.00 -0.50 alignedtext end grestore end grestore -% Environ -> Inductive -newpath 840 84 moveto -855 92 875 101 892 109 curveto +% Inductive -> Reduction +newpath 414 64 moveto +427 61 442 58 456 55 curveto stroke -newpath 893 107 moveto -901 113 lineto -891 111 lineto +newpath 456 53 moveto +466 53 lineto +457 57 lineto closepath gsave 0 setgray stroke grestore fill -% Abstraction -gsave 10 dict begin -927 18 43 18 ellipse_path +% Type_errors -> Reduction +newpath 420 27 moveto +432 29 444 32 456 35 curveto stroke -gsave 10 dict begin -927 19 moveto (Abstraction) 65 14.00 -0.50 alignedtext -end grestore -end grestore - -% Environ -> Abstraction -newpath 840 60 moveto -854 53 874 44 890 36 curveto -stroke -newpath 889 34 moveto -899 32 lineto -891 38 lineto +newpath 456 32 moveto +465 37 lineto +455 37 lineto closepath gsave 0 setgray stroke grestore fill -% Constant +% Closure gsave 10 dict begin -927 72 35 18 ellipse_path +608 45 32 18 ellipse_path stroke gsave 10 dict begin -927 73 moveto (Constant) 49 14.00 -0.50 alignedtext +608 46 moveto (Closure) 43 14.00 -0.50 alignedtext end grestore end grestore -% Environ -> Constant -newpath 848 72 moveto -859 72 871 72 882 72 curveto +% Reduction -> Closure +newpath 540 45 moveto +549 45 558 45 566 45 curveto stroke -newpath 882 70 moveto -892 72 lineto -882 75 lineto +newpath 566 43 moveto +576 45 lineto +566 48 lineto closepath gsave 0 setgray stroke grestore fill % Term gsave 10 dict begin -1125 45 27 18 ellipse_path +1229 45 27 18 ellipse_path stroke gsave 10 dict begin -1125 46 moveto (Term) 30 14.00 -0.50 alignedtext +1229 46 moveto (Term) 30 14.00 -0.50 alignedtext end grestore end grestore % Term -> Univ -newpath 1150 52 moveto -1161 55 1175 59 1187 62 curveto -stroke -newpath 1187 59 moveto -1196 65 lineto -1186 64 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Generic -gsave 10 dict begin -1221 18 32 18 ellipse_path -stroke -gsave 10 dict begin -1221 19 moveto (Generic) 44 14.00 -0.50 alignedtext -end grestore -end grestore - -% Term -> Generic -newpath 1150 38 moveto -1160 35 1171 32 1182 29 curveto -stroke -newpath 1182 26 moveto -1192 26 lineto -1183 31 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Generic -> Names -newpath 1250 26 moveto -1260 29 1273 32 1284 35 curveto -stroke -newpath 1284 32 moveto -1293 38 lineto -1283 37 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Sosub -gsave 10 dict begin -1034 18 27 18 ellipse_path +newpath 1256 45 moveto +1264 45 1273 45 1282 45 curveto stroke -gsave 10 dict begin -1034 19 moveto (Sosub) 34 14.00 -0.50 alignedtext -end grestore -end grestore - -% Sosub -> Term -newpath 1059 26 moveto -1069 29 1080 32 1091 35 curveto -stroke -newpath 1091 32 moveto -1100 38 lineto -1090 37 lineto +newpath 1282 43 moveto +1292 45 lineto +1282 48 lineto closepath gsave 0 setgray stroke grestore fill % Sign gsave 10 dict begin -1034 72 27 18 ellipse_path +1139 45 27 18 ellipse_path stroke gsave 10 dict begin -1034 73 moveto (Sign) 25 14.00 -0.50 alignedtext +1139 46 moveto (Sign) 25 14.00 -0.50 alignedtext end grestore end grestore % Sign -> Term -newpath 1059 65 moveto -1069 62 1080 58 1091 55 curveto +newpath 1166 45 moveto +1174 45 1183 45 1192 45 curveto stroke -newpath 1090 53 moveto -1100 53 lineto -1091 58 lineto +newpath 1192 43 moveto +1202 45 lineto +1192 48 lineto closepath gsave 0 setgray stroke grestore fill % Safe_typing gsave 10 dict begin -44 70 44 18 ellipse_path +44 45 44 18 ellipse_path stroke gsave 10 dict begin -44 71 moveto (Safe_typing) 67 14.00 -0.50 alignedtext +44 46 moveto (Safe_typing) 67 14.00 -0.50 alignedtext end grestore end grestore % Indtypes gsave 10 dict begin -159 70 34 18 ellipse_path +159 45 34 18 ellipse_path stroke gsave 10 dict begin -159 71 moveto (Indtypes) 48 14.00 -0.50 alignedtext +159 46 moveto (Indtypes) 48 14.00 -0.50 alignedtext end grestore end grestore % Safe_typing -> Indtypes -newpath 88 70 moveto -97 70 106 70 114 70 curveto +newpath 88 45 moveto +97 45 106 45 114 45 curveto stroke -newpath 114 68 moveto -124 70 lineto -114 73 lineto +newpath 114 43 moveto +124 45 lineto +114 48 lineto closepath gsave 0 setgray stroke grestore fill % Indtypes -> Typeops -newpath 194 70 moveto -203 70 212 70 220 70 curveto +newpath 194 45 moveto +203 45 212 45 220 45 curveto stroke -newpath 220 68 moveto -230 70 lineto -220 73 lineto +newpath 220 43 moveto +230 45 lineto +220 48 lineto closepath gsave 0 setgray stroke grestore fill % Instantiate gsave 10 dict begin -616 98 39 18 ellipse_path +716 45 39 18 ellipse_path stroke gsave 10 dict begin -616 99 moveto (Instantiate) 58 14.00 -0.50 alignedtext +716 46 moveto (Instantiate) 58 14.00 -0.50 alignedtext end grestore end grestore % Closure -> Instantiate -newpath 527 99 moveto -539 99 553 98 566 98 curveto +newpath 640 45 moveto +648 45 657 45 666 45 curveto stroke -newpath 566 96 moveto -576 98 lineto -566 101 lineto +newpath 666 43 moveto +676 45 lineto +666 48 lineto closepath gsave 0 setgray stroke grestore fill % Evd gsave 10 dict begin -719 96 27 18 ellipse_path +819 45 27 18 ellipse_path stroke gsave 10 dict begin -719 97 moveto (Evd) 22 14.00 -0.50 alignedtext +819 46 moveto (Evd) 22 14.00 -0.50 alignedtext end grestore end grestore % Instantiate -> Evd -newpath 656 97 moveto -665 97 674 97 682 97 curveto +newpath 756 45 moveto +765 45 774 45 782 45 curveto stroke -newpath 682 95 moveto -692 97 lineto -682 100 lineto +newpath 782 43 moveto +792 45 lineto +782 48 lineto closepath gsave 0 setgray stroke grestore fill +% Environ +gsave 10 dict begin +915 45 33 18 ellipse_path +stroke +gsave 10 dict begin +915 46 moveto (Environ) 45 14.00 -0.50 alignedtext +end grestore +end grestore + % Evd -> Environ -newpath 744 90 moveto -754 88 765 85 775 82 curveto +newpath 846 45 moveto +854 45 863 45 872 45 curveto stroke -newpath 775 80 moveto -785 80 lineto -776 84 lineto +newpath 872 43 moveto +882 45 lineto +872 48 lineto closepath gsave 0 setgray stroke grestore fill -% Inductive -> Sign -newpath 953 113 moveto -968 105 988 96 1004 87 curveto +% Declarations +gsave 10 dict begin +1030 45 45 18 ellipse_path stroke -newpath 1002 85 moveto -1012 83 lineto -1004 90 lineto -closepath -gsave 0 setgray stroke grestore fill +gsave 10 dict begin +1030 46 moveto (Declarations) 70 14.00 -0.50 alignedtext +end grestore +end grestore -% Abstraction -> Sosub -newpath 970 18 moveto -979 18 988 18 996 18 curveto +% Environ -> Declarations +newpath 948 45 moveto +956 45 965 45 974 45 curveto stroke -newpath 996 16 moveto -1006 18 lineto -996 21 lineto +newpath 974 43 moveto +984 45 lineto +974 48 lineto closepath gsave 0 setgray stroke grestore fill -% Constant -> Sign -newpath 962 72 moveto -974 72 986 72 997 72 curveto +% Declarations -> Sign +newpath 1076 45 moveto +1085 45 1094 45 1102 45 curveto stroke -newpath 997 70 moveto -1007 72 lineto -997 75 lineto +newpath 1102 43 moveto +1112 45 lineto +1102 48 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/library.dep.ps b/doc/library.dep.ps index a6a5fc38d..f8995d649 100644 --- a/doc/library.dep.ps +++ b/doc/library.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 429 419 +%%BoundingBox: 36 36 519 295 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,9 +139,9 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 429 419 +%%PageBoundingBox: 36 36 519 295 gsave -35 35 394 384 boxprim clip newpath +35 35 484 260 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate @@ -150,252 +150,233 @@ gsave % States gsave 10 dict begin -136 364 27 18 ellipse_path +27 217 27 18 ellipse_path stroke gsave 10 dict begin -136 365 moveto (States) 33 14.00 -0.50 alignedtext +27 218 moveto (States) 33 14.00 -0.50 alignedtext end grestore end grestore -% Lib +% Library gsave 10 dict begin -244 264 27 18 ellipse_path +122 217 31 18 ellipse_path stroke gsave 10 dict begin -244 265 moveto (Lib) 19 14.00 -0.50 alignedtext +122 218 moveto (Library) 41 14.00 -0.50 alignedtext end grestore end grestore -% States -> Lib -newpath 156 352 moveto -162 348 168 343 172 340 curveto -187 326 208 303 224 286 curveto +% States -> Library +newpath 54 217 moveto +62 217 72 217 81 217 curveto stroke -newpath 222 285 moveto -230 279 lineto -225 288 lineto +newpath 81 215 moveto +91 217 lineto +81 220 lineto closepath gsave 0 setgray stroke grestore fill -% Summary +% Global gsave 10 dict begin -354 164 37 18 ellipse_path +334 93 29 18 ellipse_path stroke gsave 10 dict begin -354 165 moveto (Summary) 54 14.00 -0.50 alignedtext +334 94 moveto (Global) 38 14.00 -0.50 alignedtext end grestore end grestore -% Lib -> Summary -newpath 260 249 moveto -279 232 308 205 329 186 curveto +% Library -> Global +newpath 145 205 moveto +176 188 231 158 262 140 curveto +274 132 291 121 306 112 curveto stroke -newpath 327 185 moveto -336 180 lineto -330 188 lineto +newpath 305 110 moveto +314 106 lineto +308 114 lineto closepath gsave 0 setgray stroke grestore fill -% Libobject +% Goptions gsave 10 dict begin -354 264 37 18 ellipse_path +226 240 36 18 ellipse_path stroke gsave 10 dict begin -354 265 moveto (Libobject) 53 14.00 -0.50 alignedtext +226 241 moveto (Goptions) 51 14.00 -0.50 alignedtext end grestore end grestore -% Lib -> Libobject -newpath 271 264 moveto -282 264 295 264 307 264 curveto +% Library -> Goptions +newpath 151 223 moveto +161 225 172 228 183 230 curveto stroke -newpath 307 262 moveto -317 264 lineto -307 267 lineto +newpath 184 228 moveto +193 232 lineto +183 232 lineto closepath gsave 0 setgray stroke grestore fill -% Redinfo +% Nametab gsave 10 dict begin -136 164 33 18 ellipse_path +334 20 35 18 ellipse_path stroke gsave 10 dict begin -136 165 moveto (Redinfo) 45 14.00 -0.50 alignedtext +334 21 moveto (Nametab) 50 14.00 -0.50 alignedtext end grestore end grestore -% Global +% Summary gsave 10 dict begin -244 164 29 18 ellipse_path +444 93 37 18 ellipse_path stroke gsave 10 dict begin -244 165 moveto (Global) 38 14.00 -0.50 alignedtext +444 94 moveto (Summary) 54 14.00 -0.50 alignedtext end grestore end grestore -% Redinfo -> Global -newpath 169 164 moveto -180 164 193 164 204 164 curveto +% Nametab -> Summary +newpath 356 34 moveto +373 45 395 61 414 73 curveto stroke -newpath 204 162 moveto -214 164 lineto -204 167 lineto +newpath 415 71 moveto +422 78 lineto +412 75 lineto closepath gsave 0 setgray stroke grestore fill % Global -> Summary -newpath 274 164 moveto -284 164 295 164 306 164 curveto -stroke -newpath 306 162 moveto -316 164 lineto -306 167 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Nametab -gsave 10 dict begin -244 87 35 18 ellipse_path -stroke -gsave 10 dict begin -244 88 moveto (Nametab) 50 14.00 -0.50 alignedtext -end grestore -end grestore - -% Nametab -> Summary -newpath 265 102 moveto -282 113 306 130 325 144 curveto +newpath 364 93 moveto +374 93 385 93 396 93 curveto stroke -newpath 326 142 moveto -333 149 lineto -323 146 lineto +newpath 396 91 moveto +406 93 lineto +396 96 lineto closepath gsave 0 setgray stroke grestore fill -% Library +% Lib gsave 10 dict begin -136 218 31 18 ellipse_path +334 156 27 18 ellipse_path stroke gsave 10 dict begin -136 219 moveto (Library) 41 14.00 -0.50 alignedtext +334 157 moveto (Lib) 19 14.00 -0.50 alignedtext end grestore end grestore -% Library -> Lib -newpath 161 229 moveto -176 235 196 244 212 251 curveto +% Goptions -> Lib +newpath 246 225 moveto +264 211 290 190 309 175 curveto stroke -newpath 212 248 moveto -221 254 lineto -211 253 lineto +newpath 306 174 moveto +316 170 lineto +309 178 lineto closepath gsave 0 setgray stroke grestore fill -% Library -> Global -newpath 160 206 moveto -175 198 196 188 213 179 curveto +% Lib -> Summary +newpath 355 144 moveto +371 135 393 122 412 112 curveto stroke -newpath 211 177 moveto -221 175 lineto -213 182 lineto +newpath 410 110 moveto +420 107 lineto +413 114 lineto closepath gsave 0 setgray stroke grestore fill -% Impargs +% Libobject gsave 10 dict begin -136 110 33 18 ellipse_path +444 156 37 18 ellipse_path stroke gsave 10 dict begin -136 111 moveto (Impargs) 45 14.00 -0.50 alignedtext +444 157 moveto (Libobject) 53 14.00 -0.50 alignedtext end grestore end grestore -% Impargs -> Global -newpath 161 122 moveto -176 130 196 140 213 148 curveto +% Lib -> Libobject +newpath 361 156 moveto +372 156 385 156 397 156 curveto stroke -newpath 213 145 moveto -221 152 lineto -211 150 lineto +newpath 397 154 moveto +407 156 lineto +397 159 lineto closepath gsave 0 setgray stroke grestore fill -% Goptions +% Impargs gsave 10 dict begin -136 310 36 18 ellipse_path +226 56 33 18 ellipse_path stroke gsave 10 dict begin -136 311 moveto (Goptions) 51 14.00 -0.50 alignedtext +226 57 moveto (Impargs) 45 14.00 -0.50 alignedtext end grestore end grestore -% Goptions -> Lib -newpath 164 298 moveto -179 292 197 284 212 278 curveto +% Impargs -> Global +newpath 254 66 moveto +268 71 285 77 299 81 curveto stroke -newpath 211 276 moveto -221 274 lineto -213 280 lineto +newpath 299 78 moveto +308 84 lineto +298 83 lineto closepath gsave 0 setgray stroke grestore fill % Declare gsave 10 dict begin -32 87 32 18 ellipse_path +122 83 32 18 ellipse_path stroke gsave 10 dict begin -32 88 moveto (Declare) 43 14.00 -0.50 alignedtext +122 84 moveto (Declare) 43 14.00 -0.50 alignedtext end grestore end grestore -% Declare -> Lib -newpath 36 105 moveto -44 140 66 219 100 248 curveto -123 266 172 268 206 267 curveto +% Declare -> Nametab +newpath 137 67 moveto +151 52 173 32 190 26 curveto +217 19 260 18 291 18 curveto stroke -newpath 207 264 moveto -217 266 lineto -207 269 lineto +newpath 288 16 moveto +298 18 lineto +288 21 lineto closepath gsave 0 setgray stroke grestore fill -% Declare -> Nametab -newpath 64 84 moveto -76 82 90 81 100 80 curveto -126 79 168 81 199 83 curveto +% Declare -> Lib +newpath 137 99 moveto +151 114 173 134 190 140 curveto +219 149 267 153 300 155 curveto stroke -newpath 199 81 moveto -209 84 lineto -199 85 lineto +newpath 297 153 moveto +307 155 lineto +297 158 lineto closepath gsave 0 setgray stroke grestore fill % Declare -> Impargs -newpath 62 94 moveto -73 96 85 99 96 101 curveto +newpath 151 75 moveto +162 72 175 69 187 66 curveto stroke -newpath 96 98 moveto -105 103 lineto -95 103 lineto +newpath 186 64 moveto +196 64 lineto +187 69 lineto closepath gsave 0 setgray stroke grestore fill % Indrec gsave 10 dict begin -136 18 28 18 ellipse_path +226 110 28 18 ellipse_path stroke gsave 10 dict begin -136 19 moveto (Indrec) 35 14.00 -0.50 alignedtext +226 111 moveto (Indrec) 35 14.00 -0.50 alignedtext end grestore end grestore % Declare -> Indrec -newpath 53 73 moveto -69 63 91 48 108 36 curveto +newpath 151 91 moveto +163 94 178 98 191 101 curveto stroke -newpath 106 34 moveto -116 31 lineto -109 38 lineto +newpath 191 98 moveto +200 103 lineto +190 103 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps index de816c0af..97d69aa0d 100644 --- a/doc/parsing.dep.ps +++ b/doc/parsing.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 183 +%%BoundingBox: 36 36 577 217 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,283 +139,314 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 183 +%%PageBoundingBox: 36 36 577 217 gsave -35 35 541 148 boxprim clip newpath +35 35 542 182 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7988 set_scale +0.8060 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font -% Termast +% Pcoq gsave 10 dict begin -367 160 33 18 ellipse_path +547 110 27 18 ellipse_path stroke gsave 10 dict begin -367 161 moveto (Termast) 45 14.00 -0.50 alignedtext +547 111 moveto (Pcoq) 28 14.00 -0.50 alignedtext end grestore end grestore -% Ast +% Coqast gsave 10 dict begin -463 83 27 18 ellipse_path +640 110 30 18 ellipse_path stroke gsave 10 dict begin -463 84 moveto (Ast) 19 14.00 -0.50 alignedtext +640 111 moveto (Coqast) 38 14.00 -0.50 alignedtext end grestore end grestore -% Termast -> Ast -newpath 386 145 moveto -401 133 422 116 438 103 curveto +% Pcoq -> Coqast +newpath 574 110 moveto +582 110 591 110 600 110 curveto stroke -newpath 436 102 moveto -445 97 lineto -439 105 lineto +newpath 600 108 moveto +610 110 lineto +600 113 lineto closepath gsave 0 setgray stroke grestore fill -% Pcoq +% Extend gsave 10 dict begin -553 83 27 18 ellipse_path +364 110 30 18 ellipse_path stroke gsave 10 dict begin -553 84 moveto (Pcoq) 28 14.00 -0.50 alignedtext +364 111 moveto (Extend) 39 14.00 -0.50 alignedtext end grestore end grestore -% Ast -> Pcoq -newpath 490 83 moveto -498 83 507 83 516 83 curveto -stroke -newpath 516 81 moveto -526 83 lineto -516 86 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Printer +% Ast gsave 10 dict begin -136 166 29 18 ellipse_path +457 110 27 18 ellipse_path stroke gsave 10 dict begin -136 167 moveto (Printer) 38 14.00 -0.50 alignedtext +457 111 moveto (Ast) 19 14.00 -0.50 alignedtext end grestore end grestore -% Printer -> Termast -newpath 166 165 moveto -206 164 278 162 325 161 curveto +% Extend -> Ast +newpath 394 110 moveto +402 110 411 110 420 110 curveto stroke -newpath 324 159 moveto -334 161 lineto -324 164 lineto +newpath 420 108 moveto +430 110 lineto +420 113 lineto closepath gsave 0 setgray stroke grestore fill -% Esyntax +% Ast -> Pcoq +newpath 484 110 moveto +492 110 501 110 510 110 curveto +stroke +newpath 510 108 moveto +520 110 lineto +510 113 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Termast gsave 10 dict begin -258 126 33 18 ellipse_path +258 44 33 18 ellipse_path stroke gsave 10 dict begin -258 127 moveto (Esyntax) 45 14.00 -0.50 alignedtext +258 45 moveto (Termast) 45 14.00 -0.50 alignedtext end grestore end grestore -% Printer -> Esyntax -newpath 162 157 moveto -179 152 202 144 221 138 curveto +% Termast -> Ast +newpath 285 34 moveto +317 23 369 9 394 26 curveto +411 38 430 65 442 85 curveto stroke -newpath 220 136 moveto -230 135 lineto -221 141 lineto +newpath 444 83 moveto +447 93 lineto +440 86 lineto closepath gsave 0 setgray stroke grestore fill -% Extend +% Pattern gsave 10 dict begin -367 83 30 18 ellipse_path +364 56 30 18 ellipse_path stroke gsave 10 dict begin -367 84 moveto (Extend) 39 14.00 -0.50 alignedtext +364 57 moveto (Pattern) 39 14.00 -0.50 alignedtext end grestore end grestore -% Esyntax -> Extend -newpath 285 115 moveto -299 110 318 103 333 97 curveto +% Termast -> Pattern +newpath 290 48 moveto +301 49 313 50 325 52 curveto stroke -newpath 332 95 moveto -342 93 lineto -334 99 lineto +newpath 324 49 moveto +334 53 lineto +324 54 lineto closepath gsave 0 setgray stroke grestore fill -% Pretty +% Printer gsave 10 dict begin -27 166 27 18 ellipse_path +136 44 29 18 ellipse_path stroke gsave 10 dict begin -27 167 moveto (Pretty) 33 14.00 -0.50 alignedtext +136 45 moveto (Printer) 38 14.00 -0.50 alignedtext end grestore end grestore -% Pretty -> Printer -newpath 54 166 moveto -67 166 82 166 96 166 curveto +% Printer -> Termast +newpath 166 44 moveto +181 44 199 44 215 44 curveto stroke -newpath 96 164 moveto -106 166 lineto -96 169 lineto +newpath 215 42 moveto +225 44 lineto +215 47 lineto closepath gsave 0 setgray stroke grestore fill -% Coqast +% Esyntax gsave 10 dict begin -646 110 30 18 ellipse_path +258 98 33 18 ellipse_path stroke gsave 10 dict begin -646 111 moveto (Coqast) 38 14.00 -0.50 alignedtext +258 99 moveto (Esyntax) 45 14.00 -0.50 alignedtext end grestore end grestore -% Pcoq -> Coqast -newpath 578 90 moveto -587 93 599 96 609 99 curveto +% Printer -> Esyntax +newpath 160 55 moveto +178 63 204 74 224 83 curveto stroke -newpath 610 97 moveto -619 102 lineto -609 102 lineto +newpath 224 80 moveto +232 87 lineto +222 85 lineto closepath gsave 0 setgray stroke grestore fill -% Lexer +% Esyntax -> Extend +newpath 290 102 moveto +301 103 313 104 325 106 curveto +stroke +newpath 324 103 moveto +334 107 lineto +324 108 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Pretty gsave 10 dict begin -646 56 27 18 ellipse_path +27 44 27 18 ellipse_path stroke gsave 10 dict begin -646 57 moveto (Lexer) 32 14.00 -0.50 alignedtext +27 45 moveto (Pretty) 33 14.00 -0.50 alignedtext end grestore end grestore -% Pcoq -> Lexer -newpath 578 76 moveto -588 73 601 69 612 66 curveto +% Pretty -> Printer +newpath 54 44 moveto +67 44 82 44 96 44 curveto stroke -newpath 611 64 moveto -621 63 lineto -612 69 lineto +newpath 96 42 moveto +106 44 lineto +96 47 lineto closepath gsave 0 setgray stroke grestore fill % G_zsyntax gsave 10 dict begin -136 24 40 18 ellipse_path +136 152 40 18 ellipse_path stroke gsave 10 dict begin -136 25 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext +136 153 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext end grestore end grestore % G_zsyntax -> Esyntax -newpath 158 39 moveto -167 46 176 53 182 59 curveto -196 72 204 90 218 102 curveto -220 104 222 106 225 108 curveto +newpath 165 139 moveto +182 131 206 121 224 113 curveto stroke -newpath 226 106 moveto -234 113 lineto -224 110 lineto +newpath 222 111 moveto +232 109 lineto +224 116 lineto closepath gsave 0 setgray stroke grestore fill % Astterm gsave 10 dict begin -258 18 33 18 ellipse_path +258 152 33 18 ellipse_path stroke gsave 10 dict begin -258 19 moveto (Astterm) 45 14.00 -0.50 alignedtext +258 153 moveto (Astterm) 45 14.00 -0.50 alignedtext end grestore end grestore % G_zsyntax -> Astterm -newpath 176 22 moveto -189 21 203 20 215 20 curveto +newpath 176 152 moveto +189 152 203 152 215 152 curveto stroke -newpath 215 18 moveto -225 20 lineto -215 23 lineto +newpath 215 150 moveto +225 152 lineto +215 155 lineto closepath gsave 0 setgray stroke grestore fill % Astterm -> Ast -newpath 289 25 moveto -321 32 371 44 400 53 curveto -409 56 421 62 433 67 curveto +newpath 291 150 moveto +322 149 367 146 394 140 curveto +394 140 411 132 427 124 curveto +stroke +newpath 425 122 moveto +435 120 lineto +427 127 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Astterm -> Pattern +newpath 282 139 moveto +288 136 294 132 298 128 curveto +313 114 321 94 334 80 curveto +334 80 336 79 339 77 curveto stroke -newpath 434 65 moveto -442 72 lineto -432 69 lineto +newpath 337 76 moveto +346 71 lineto +340 79 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax gsave 10 dict begin -136 89 45 18 ellipse_path +136 98 45 18 ellipse_path stroke gsave 10 dict begin -136 90 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext +136 99 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext end grestore end grestore % G_natsyntax -> Esyntax -newpath 172 100 moveto -187 105 205 110 220 114 curveto +newpath 182 98 moveto +193 98 205 98 216 98 curveto stroke -newpath 220 111 moveto -229 117 lineto -219 116 lineto +newpath 215 96 moveto +225 98 lineto +215 101 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax -> Astterm -newpath 162 74 moveto -181 63 207 47 227 35 curveto +newpath 166 111 moveto +184 119 206 129 224 137 curveto stroke -newpath 225 33 moveto -235 31 lineto -227 38 lineto +newpath 224 134 moveto +233 140 lineto +223 139 lineto closepath gsave 0 setgray stroke grestore fill -% Extend -> Ast -newpath 397 83 moveto -406 83 417 83 426 83 curveto +% Egrammar +gsave 10 dict begin +258 206 40 18 ellipse_path stroke -newpath 426 81 moveto -436 83 lineto -426 86 lineto +gsave 10 dict begin +258 207 moveto (Egrammar) 58 14.00 -0.50 alignedtext +end grestore +end grestore + +% Egrammar -> Extend +newpath 284 192 moveto +289 189 295 185 298 182 curveto +312 170 330 149 344 133 curveto +stroke +newpath 342 132 moveto +350 126 lineto +345 135 lineto closepath gsave 0 setgray stroke grestore fill -% Egrammar +% Lexer gsave 10 dict begin -258 72 40 18 ellipse_path +364 206 27 18 ellipse_path stroke gsave 10 dict begin -258 73 moveto (Egrammar) 58 14.00 -0.50 alignedtext +364 207 moveto (Lexer) 32 14.00 -0.50 alignedtext end grestore end grestore -% Egrammar -> Extend -newpath 297 76 moveto -307 77 318 78 328 79 curveto +% Egrammar -> Lexer +newpath 298 206 moveto +308 206 318 206 327 206 curveto stroke -newpath 327 76 moveto -337 80 lineto -327 81 lineto +newpath 327 204 moveto +337 206 lineto +327 209 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps index 6a06d166f..9e5348ac4 100644 --- a/doc/pretyping.dep.ps +++ b/doc/pretyping.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 199 +%%BoundingBox: 36 36 577 188 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,293 +139,332 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 199 +%%PageBoundingBox: 36 36 577 188 gsave -35 35 541 164 boxprim clip newpath +35 35 542 153 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.8207 set_scale +0.6308 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Multcase gsave 10 dict begin -257 72 36 18 ellipse_path +347 70 36 18 ellipse_path stroke gsave 10 dict begin -257 73 moveto (Multcase) 51 14.00 -0.50 alignedtext +347 71 moveto (Multcase) 51 14.00 -0.50 alignedtext end grestore end grestore % Evarutil gsave 10 dict begin -370 72 33 18 ellipse_path +460 72 33 18 ellipse_path stroke gsave 10 dict begin -370 73 moveto (Evarutil) 45 14.00 -0.50 alignedtext +460 73 moveto (Evarutil) 45 14.00 -0.50 alignedtext end grestore end grestore % Multcase -> Evarutil -newpath 293 72 moveto -304 72 316 72 327 72 curveto +newpath 383 71 moveto +394 71 406 71 417 71 curveto stroke -newpath 327 70 moveto -337 72 lineto -327 75 lineto +newpath 417 69 moveto +427 71 lineto +417 74 lineto closepath gsave 0 setgray stroke grestore fill % Pretype_errors gsave 10 dict begin -498 45 51 18 ellipse_path +588 72 51 18 ellipse_path stroke gsave 10 dict begin -498 46 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext +588 73 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext end grestore end grestore % Evarutil -> Pretype_errors -newpath 401 65 moveto -414 63 429 59 443 56 curveto +newpath 493 72 moveto +503 72 515 72 526 72 curveto stroke -newpath 443 54 moveto -453 54 lineto -444 58 lineto +newpath 526 70 moveto +536 72 lineto +526 75 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Tacred +gsave 10 dict begin +712 180 29 18 ellipse_path +stroke +gsave 10 dict begin +712 181 moveto (Tacred) 38 14.00 -0.50 alignedtext +end grestore +end grestore + +% Retyping +gsave 10 dict begin +820 180 36 18 ellipse_path +stroke +gsave 10 dict begin +820 181 moveto (Retyping) 51 14.00 -0.50 alignedtext +end grestore +end grestore + +% Tacred -> Retyping +newpath 742 180 moveto +752 180 763 180 774 180 curveto +stroke +newpath 774 178 moveto +784 180 lineto +774 183 lineto closepath gsave 0 setgray stroke grestore fill % Syntax_def gsave 10 dict begin -498 99 42 18 ellipse_path +588 126 42 18 ellipse_path stroke gsave 10 dict begin -498 100 moveto (Syntax_def) 63 14.00 -0.50 alignedtext +588 127 moveto (Syntax_def) 63 14.00 -0.50 alignedtext end grestore end grestore % Rawterm gsave 10 dict begin -622 72 36 18 ellipse_path +712 99 36 18 ellipse_path stroke gsave 10 dict begin -622 73 moveto (Rawterm) 51 14.00 -0.50 alignedtext +712 100 moveto (Rawterm) 51 14.00 -0.50 alignedtext end grestore end grestore % Syntax_def -> Rawterm -newpath 536 91 moveto -550 88 565 84 579 81 curveto +newpath 626 118 moveto +640 115 655 111 669 108 curveto stroke -newpath 579 79 moveto -589 79 lineto -580 83 lineto +newpath 669 106 moveto +679 106 lineto +670 110 lineto closepath gsave 0 setgray stroke grestore fill % Recordops gsave 10 dict begin -370 126 40 18 ellipse_path +460 222 40 18 ellipse_path stroke gsave 10 dict begin -370 127 moveto (Recordops) 59 14.00 -0.50 alignedtext +460 223 moveto (Recordops) 59 14.00 -0.50 alignedtext end grestore end grestore % Classops gsave 10 dict begin -498 153 35 18 ellipse_path +588 180 35 18 ellipse_path stroke gsave 10 dict begin -498 154 moveto (Classops) 49 14.00 -0.50 alignedtext +588 181 moveto (Classops) 49 14.00 -0.50 alignedtext end grestore end grestore % Recordops -> Classops -newpath 406 134 moveto -422 137 440 141 456 144 curveto +newpath 493 211 moveto +510 206 532 199 549 193 curveto stroke -newpath 456 141 moveto -465 146 lineto -455 146 lineto +newpath 548 191 moveto +558 190 lineto +549 196 lineto closepath gsave 0 setgray stroke grestore fill -% Tacred -gsave 10 dict begin -622 153 29 18 ellipse_path +% Classops -> Tacred +newpath 623 180 moveto +639 180 657 180 673 180 curveto stroke -gsave 10 dict begin -622 154 moveto (Tacred) 38 14.00 -0.50 alignedtext -end grestore -end grestore +newpath 672 178 moveto +682 180 lineto +672 183 lineto +closepath +gsave 0 setgray stroke grestore fill -% Classops -> Tacred -newpath 533 153 moveto -549 153 567 153 583 153 curveto +% Classops -> Rawterm +newpath 615 169 moveto +625 165 634 160 640 156 curveto +654 147 672 133 687 121 curveto stroke -newpath 582 151 moveto -592 153 lineto -582 156 lineto +newpath 685 120 moveto +694 115 lineto +688 123 lineto closepath gsave 0 setgray stroke grestore fill % Pretyping gsave 10 dict begin -38 72 37 18 ellipse_path +38 178 37 18 ellipse_path stroke gsave 10 dict begin -38 73 moveto (Pretyping) 54 14.00 -0.50 alignedtext +38 179 moveto (Pretyping) 54 14.00 -0.50 alignedtext end grestore end grestore % Cases gsave 10 dict begin -148 99 27 18 ellipse_path +139 178 27 18 ellipse_path stroke gsave 10 dict begin -148 100 moveto (Cases) 32 14.00 -0.50 alignedtext +139 179 moveto (Cases) 32 14.00 -0.50 alignedtext end grestore end grestore % Pretyping -> Cases -newpath 72 80 moveto -85 83 101 87 114 91 curveto +newpath 76 178 moveto +85 178 94 178 102 178 curveto stroke -newpath 114 88 moveto -123 93 lineto -113 93 lineto +newpath 102 176 moveto +112 178 lineto +102 181 lineto closepath gsave 0 setgray stroke grestore fill % Coercion gsave 10 dict begin -148 45 36 18 ellipse_path +238 178 36 18 ellipse_path stroke gsave 10 dict begin -148 46 moveto (Coercion) 51 14.00 -0.50 alignedtext +238 179 moveto (Coercion) 51 14.00 -0.50 alignedtext end grestore end grestore -% Pretyping -> Coercion -newpath 72 64 moveto -83 62 95 59 106 56 curveto +% Cases -> Coercion +newpath 166 178 moveto +174 178 183 178 192 178 curveto stroke -newpath 105 54 moveto -115 53 lineto -106 59 lineto +newpath 192 176 moveto +202 178 lineto +192 181 lineto closepath gsave 0 setgray stroke grestore fill -% Evarconv -gsave 10 dict begin -257 126 37 18 ellipse_path -stroke -gsave 10 dict begin -257 127 moveto (Evarconv) 53 14.00 -0.50 alignedtext -end grestore -end grestore - -% Cases -> Evarconv -newpath 174 105 moveto -186 108 201 112 214 116 curveto +% Pretype_errors -> Rawterm +newpath 632 82 moveto +644 84 657 87 669 90 curveto stroke -newpath 215 114 moveto -224 118 lineto -214 118 lineto +newpath 670 88 moveto +679 92 lineto +669 92 lineto closepath gsave 0 setgray stroke grestore fill -% Retyping +% Evarconv gsave 10 dict begin -257 18 36 18 ellipse_path +347 178 37 18 ellipse_path stroke gsave 10 dict begin -257 19 moveto (Retyping) 51 14.00 -0.50 alignedtext +347 179 moveto (Evarconv) 53 14.00 -0.50 alignedtext end grestore end grestore -% Cases -> Retyping -newpath 167 86 moveto -174 82 180 78 184 75 curveto -197 64 208 52 220 42 curveto -222 40 225 38 228 36 curveto +% Evarconv -> Evarutil +newpath 371 164 moveto +376 161 381 157 384 154 curveto +400 140 423 114 440 95 curveto stroke -newpath 224 35 moveto -234 32 lineto -227 40 lineto +newpath 437 94 moveto +446 89 lineto +441 98 lineto closepath gsave 0 setgray stroke grestore fill -% Coercion -> Evarconv -newpath 170 59 moveto -176 63 180 66 184 69 curveto -197 79 208 91 220 102 curveto -222 104 225 106 228 108 curveto -stroke -newpath 227 104 moveto -234 112 lineto -224 109 lineto +% Evarconv -> Recordops +newpath 376 189 moveto +390 194 406 200 421 206 curveto +stroke +newpath 422 204 moveto +430 210 lineto +420 208 lineto closepath gsave 0 setgray stroke grestore fill -% Coercion -> Retyping -newpath 180 37 moveto -191 35 204 31 216 28 curveto +% Typing +gsave 10 dict begin +460 168 30 18 ellipse_path stroke -newpath 215 26 moveto -225 26 lineto -216 31 lineto -closepath -gsave 0 setgray stroke grestore fill +gsave 10 dict begin +460 169 moveto (Typing) 40 14.00 -0.50 alignedtext +end grestore +end grestore -% Pretype_errors -> Rawterm -newpath 542 55 moveto -554 57 567 60 579 63 curveto +% Evarconv -> Typing +newpath 384 175 moveto +396 174 409 173 421 172 curveto stroke -newpath 580 61 moveto -589 65 lineto -579 65 lineto +newpath 420 170 moveto +430 171 lineto +420 175 lineto closepath gsave 0 setgray stroke grestore fill -% Evarconv -> Evarutil -newpath 283 113 moveto -299 105 320 95 337 88 curveto +% Detyping +gsave 10 dict begin +588 18 36 18 ellipse_path +stroke +gsave 10 dict begin +588 19 moveto (Detyping) 52 14.00 -0.50 alignedtext +end grestore +end grestore + +% Detyping -> Rawterm +newpath 616 30 moveto +625 34 634 38 640 42 curveto +653 51 671 65 687 77 curveto stroke -newpath 335 86 moveto -345 84 lineto -337 91 lineto +newpath 688 75 moveto +694 83 lineto +685 78 lineto closepath gsave 0 setgray stroke grestore fill -% Evarconv -> Recordops -newpath 294 126 moveto -302 126 311 126 320 126 curveto +% Coercion -> Evarconv +newpath 274 178 moveto +282 178 291 178 300 178 curveto stroke -newpath 320 124 moveto -330 126 lineto -320 129 lineto +newpath 300 176 moveto +310 178 lineto +300 181 lineto closepath gsave 0 setgray stroke grestore fill -% Typing +% Class gsave 10 dict begin -370 180 30 18 ellipse_path +347 124 27 18 ellipse_path stroke gsave 10 dict begin -370 181 moveto (Typing) 40 14.00 -0.50 alignedtext +347 125 moveto (Class) 30 14.00 -0.50 alignedtext end grestore end grestore -% Evarconv -> Typing -newpath 283 139 moveto -299 147 321 157 338 165 curveto +% Class -> Classops +newpath 374 126 moveto +408 128 466 133 500 138 curveto +514 141 524 150 536 156 curveto +541 158 549 162 556 165 curveto +stroke +newpath 554 161 moveto +562 168 lineto +552 166 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Class -> Typing +newpath 370 133 moveto +386 139 408 147 425 154 curveto stroke -newpath 338 162 moveto -346 169 lineto -336 167 lineto +newpath 426 152 moveto +434 158 lineto +424 156 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps index 9f92d1e95..b8f9a065e 100644 --- a/doc/proofs.dep.ps +++ b/doc/proofs.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 145 +%%BoundingBox: 36 36 577 129 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,12 +139,12 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 145 +%%PageBoundingBox: 36 36 577 129 gsave -35 35 541 110 boxprim clip newpath +35 35 542 94 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7521 set_scale +0.6444 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font @@ -272,6 +272,25 @@ newpath 622 70 moveto closepath gsave 0 setgray stroke grestore fill +% Proof_type +gsave 10 dict begin +796 72 41 18 ellipse_path +stroke +gsave 10 dict begin +796 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext +end grestore +end grestore + +% Proof_trees -> Proof_type +newpath 718 72 moveto +727 72 736 72 744 72 curveto +stroke +newpath 744 70 moveto +754 72 lineto +744 75 lineto +closepath +gsave 0 setgray stroke grestore fill + % Pfedit gsave 10 dict begin 141 72 27 18 ellipse_path diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps index 0ff40bcdc..940e81966 100644 --- a/doc/tactics.dep.ps +++ b/doc/tactics.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 152 +%%BoundingBox: 36 36 577 194 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,279 +139,396 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 152 +%%PageBoundingBox: 36 36 577 194 gsave -35 35 541 117 boxprim clip newpath +35 35 542 159 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7563 set_scale +0.6618 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Termdn gsave 10 dict begin -462 18 32 18 ellipse_path +653 202 32 18 ellipse_path stroke gsave 10 dict begin -462 19 moveto (Termdn) 44 14.00 -0.50 alignedtext +653 203 moveto (Termdn) 44 14.00 -0.50 alignedtext end grestore end grestore % Dn gsave 10 dict begin -579 18 27 18 ellipse_path +771 202 27 18 ellipse_path stroke gsave 10 dict begin -579 19 moveto (Dn) 17 14.00 -0.50 alignedtext +771 203 moveto (Dn) 17 14.00 -0.50 alignedtext end grestore end grestore % Termdn -> Dn -newpath 495 18 moveto -510 18 527 18 543 18 curveto +newpath 686 202 moveto +701 202 719 202 735 202 curveto stroke -newpath 542 16 moveto -552 18 lineto -542 21 lineto +newpath 734 200 moveto +744 202 lineto +734 205 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Tauto +gsave 10 dict begin +127 220 27 18 ellipse_path +stroke +gsave 10 dict begin +127 221 moveto (Tauto) 32 14.00 -0.50 alignedtext +end grestore +end grestore + +% Auto +gsave 10 dict begin +217 166 27 18 ellipse_path +stroke +gsave 10 dict begin +217 167 moveto (Auto) 28 14.00 -0.50 alignedtext +end grestore +end grestore + +% Tauto -> Auto +newpath 147 208 moveto +159 201 175 191 189 183 curveto +stroke +newpath 187 181 moveto +197 178 lineto +190 185 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Hiddentac +gsave 10 dict begin +319 114 39 18 ellipse_path +stroke +gsave 10 dict begin +319 115 moveto (Hiddentac) 57 14.00 -0.50 alignedtext +end grestore +end grestore + +% Auto -> Hiddentac +newpath 239 155 moveto +252 148 269 140 284 132 curveto +stroke +newpath 283 130 moveto +293 128 lineto +285 134 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Dhyp +gsave 10 dict begin +319 168 27 18 ellipse_path +stroke +gsave 10 dict begin +319 169 moveto (Dhyp) 31 14.00 -0.50 alignedtext +end grestore +end grestore + +% Auto -> Dhyp +newpath 244 167 moveto +256 167 270 167 282 167 curveto +stroke +newpath 282 165 moveto +292 167 lineto +282 170 lineto closepath gsave 0 setgray stroke grestore fill % Tactics gsave 10 dict begin -355 91 30 18 ellipse_path +545 87 30 18 ellipse_path stroke gsave 10 dict begin -355 92 moveto (Tactics) 40 14.00 -0.50 alignedtext +545 88 moveto (Tactics) 40 14.00 -0.50 alignedtext end grestore end grestore -% Tacticals +% Hipattern gsave 10 dict begin -462 91 35 18 ellipse_path +653 114 36 18 ellipse_path stroke gsave 10 dict begin -462 92 moveto (Tacticals) 50 14.00 -0.50 alignedtext +653 115 moveto (Hipattern) 52 14.00 -0.50 alignedtext end grestore end grestore -% Tactics -> Tacticals -newpath 386 91 moveto -395 91 406 91 416 91 curveto +% Tactics -> Hipattern +newpath 573 94 moveto +584 97 598 100 610 104 curveto stroke -newpath 416 89 moveto -426 91 lineto -416 94 lineto +newpath 611 102 moveto +620 106 lineto +610 106 lineto closepath gsave 0 setgray stroke grestore fill -% Pattern +% Tacticals gsave 10 dict begin -579 135 30 18 ellipse_path +653 60 35 18 ellipse_path stroke gsave 10 dict begin -579 136 moveto (Pattern) 39 14.00 -0.50 alignedtext +653 61 moveto (Tacticals) 50 14.00 -0.50 alignedtext end grestore end grestore -% Tacticals -> Pattern -newpath 491 102 moveto -507 108 528 116 544 122 curveto +% Tactics -> Tacticals +newpath 573 80 moveto +585 77 599 74 612 70 curveto stroke -newpath 544 119 moveto -553 125 lineto -543 124 lineto +newpath 611 68 moveto +621 68 lineto +612 73 lineto closepath gsave 0 setgray stroke grestore fill % Wcclausenv gsave 10 dict begin -579 81 44 18 ellipse_path +771 60 44 18 ellipse_path stroke gsave 10 dict begin -579 82 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext +771 61 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext end grestore end grestore % Tacticals -> Wcclausenv -newpath 497 88 moveto -506 87 516 87 525 86 curveto +newpath 689 60 moveto +698 60 707 60 716 60 curveto stroke -newpath 525 84 moveto -535 85 lineto -525 88 lineto +newpath 716 58 moveto +726 60 lineto +716 63 lineto closepath gsave 0 setgray stroke grestore fill -% Stock +% Tacentries gsave 10 dict begin -687 135 27 18 ellipse_path +434 110 39 18 ellipse_path stroke gsave 10 dict begin -687 136 moveto (Stock) 31 14.00 -0.50 alignedtext +434 111 moveto (Tacentries) 58 14.00 -0.50 alignedtext end grestore end grestore -% Pattern -> Stock -newpath 609 135 moveto -622 135 637 135 650 135 curveto +% Tacentries -> Tactics +newpath 470 103 moveto +482 101 495 98 507 95 curveto stroke -newpath 650 133 moveto -660 135 lineto -650 138 lineto +newpath 506 93 moveto +516 93 lineto +507 98 lineto closepath gsave 0 setgray stroke grestore fill -% Tacentries +% Refine gsave 10 dict begin -244 110 39 18 ellipse_path +434 18 29 18 ellipse_path stroke gsave 10 dict begin -244 111 moveto (Tacentries) 58 14.00 -0.50 alignedtext +434 19 moveto (Refine) 37 14.00 -0.50 alignedtext end grestore end grestore -% Tacentries -> Tactics -newpath 281 104 moveto -293 102 305 99 317 97 curveto +% Refine -> Tactics +newpath 455 31 moveto +473 42 497 57 516 69 curveto stroke -newpath 316 95 moveto -326 96 lineto -316 100 lineto +newpath 517 67 moveto +524 74 lineto +514 71 lineto closepath gsave 0 setgray stroke grestore fill % Nbtermdn gsave 10 dict begin -244 18 38 18 ellipse_path +434 202 38 18 ellipse_path stroke gsave 10 dict begin -244 19 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext +434 203 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext end grestore end grestore % Btermdn gsave 10 dict begin -355 18 35 18 ellipse_path +545 202 35 18 ellipse_path stroke gsave 10 dict begin -355 19 moveto (Btermdn) 49 14.00 -0.50 alignedtext +545 203 moveto (Btermdn) 49 14.00 -0.50 alignedtext end grestore end grestore % Nbtermdn -> Btermdn -newpath 283 18 moveto -292 18 301 18 310 18 curveto +newpath 473 202 moveto +482 202 491 202 500 202 curveto stroke -newpath 310 16 moveto -320 18 lineto -310 21 lineto +newpath 500 200 moveto +510 202 lineto +500 205 lineto closepath gsave 0 setgray stroke grestore fill % Btermdn -> Termdn -newpath 390 18 moveto -400 18 410 18 419 18 curveto +newpath 580 202 moveto +590 202 601 202 611 202 curveto stroke -newpath 419 16 moveto -429 18 lineto -419 21 lineto +newpath 610 200 moveto +620 202 lineto +610 205 lineto closepath gsave 0 setgray stroke grestore fill -% Hiddentac +% Leminv gsave 10 dict begin -129 110 39 18 ellipse_path +32 112 32 18 ellipse_path stroke gsave 10 dict begin -129 111 moveto (Hiddentac) 57 14.00 -0.50 alignedtext +32 113 moveto (Leminv) 43 14.00 -0.50 alignedtext end grestore end grestore -% Hiddentac -> Tacentries -newpath 168 110 moveto -177 110 186 110 194 110 curveto +% Inv +gsave 10 dict begin +127 112 27 18 ellipse_path stroke -newpath 194 108 moveto -204 110 lineto -194 113 lineto +gsave 10 dict begin +127 113 moveto (Inv) 18 14.00 -0.50 alignedtext +end grestore +end grestore + +% Leminv -> Inv +newpath 64 112 moveto +73 112 82 112 90 112 curveto +stroke +newpath 90 110 moveto +100 112 lineto +90 115 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Inv -> Auto +newpath 147 124 moveto +159 131 175 141 189 149 curveto +stroke +newpath 190 147 moveto +197 154 lineto +187 151 lineto closepath gsave 0 setgray stroke grestore fill % Elim gsave 10 dict begin -27 110 27 18 ellipse_path +217 112 27 18 ellipse_path stroke gsave 10 dict begin -27 111 moveto (Elim) 27 14.00 -0.50 alignedtext +217 113 moveto (Elim) 27 14.00 -0.50 alignedtext end grestore end grestore -% Elim -> Hiddentac -newpath 54 110 moveto -62 110 71 110 80 110 curveto +% Inv -> Elim +newpath 154 112 moveto +162 112 171 112 180 112 curveto stroke -newpath 80 108 moveto -90 110 lineto -80 113 lineto +newpath 180 110 moveto +190 112 lineto +180 115 lineto closepath gsave 0 setgray stroke grestore fill -% Dhyp +% Equality gsave 10 dict begin -129 56 27 18 ellipse_path +319 60 34 18 ellipse_path stroke gsave 10 dict begin -129 57 moveto (Dhyp) 31 14.00 -0.50 alignedtext +319 61 moveto (Equality) 47 14.00 -0.50 alignedtext end grestore end grestore -% Dhyp -> Tactics -newpath 155 60 moveto -195 66 270 77 316 85 curveto +% Inv -> Equality +newpath 148 101 moveto +161 93 178 85 190 82 curveto +213 76 249 69 277 65 curveto stroke -newpath 315 82 moveto -325 86 lineto -315 87 lineto +newpath 276 63 moveto +286 64 lineto +276 68 lineto closepath gsave 0 setgray stroke grestore fill -% Dhyp -> Nbtermdn -newpath 153 48 moveto -167 43 187 37 204 31 curveto +% Elim -> Hiddentac +newpath 244 113 moveto +252 113 261 113 270 113 curveto stroke -newpath 203 29 moveto -213 28 lineto -204 34 lineto +newpath 270 111 moveto +280 113 lineto +270 116 lineto closepath gsave 0 setgray stroke grestore fill -% Auto +% Equality -> Tactics +newpath 352 64 moveto +393 69 463 77 506 82 curveto +stroke +newpath 505 79 moveto +515 83 lineto +505 84 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Hiddentac -> Tacentries +newpath 358 113 moveto +367 112 375 112 384 112 curveto +stroke +newpath 384 110 moveto +394 111 lineto +384 114 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Eauto gsave 10 dict begin -27 56 27 18 ellipse_path +127 166 27 18 ellipse_path stroke gsave 10 dict begin -27 57 moveto (Auto) 28 14.00 -0.50 alignedtext +127 167 moveto (Eauto) 32 14.00 -0.50 alignedtext end grestore end grestore -% Auto -> Hiddentac -newpath 49 67 moveto -62 75 80 84 95 92 curveto +% Eauto -> Auto +newpath 154 166 moveto +162 166 171 166 180 166 curveto stroke -newpath 96 90 moveto -104 96 lineto -94 94 lineto +newpath 180 164 moveto +190 166 lineto +180 169 lineto closepath gsave 0 setgray stroke grestore fill -% Auto -> Dhyp -newpath 54 56 moveto -66 56 80 56 92 56 curveto +% Dhyp -> Tactics +newpath 346 165 moveto +380 160 441 152 474 140 curveto +488 135 507 121 521 108 curveto +stroke +newpath 519 107 moveto +528 102 lineto +522 110 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Dhyp -> Nbtermdn +newpath 344 175 moveto +358 179 376 185 392 189 curveto stroke -newpath 92 54 moveto -102 56 lineto -92 59 lineto +newpath 392 186 moveto +401 192 lineto +391 191 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps index 28aae6299..a57446d80 100644 --- a/doc/toplevel.dep.ps +++ b/doc/toplevel.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 %%Creator: dot version uwin98 (01-26-98) -%%For: (jc) Jean-Christophe,,,, +%%For: (jacek) Jacek Chrzaszcz %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 218 +%%BoundingBox: 36 36 577 240 %%EndComments %%BeginProlog save @@ -47,7 +47,7 @@ DotDict begin gsave coordfont setfont 0 0 moveto - (() show i str cvs show (,) show j str cvs show ()) show + (\() show i str cvs show (,) show j str cvs show (\)) show grestore } if } bind def @@ -139,12 +139,12 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 218 +%%PageBoundingBox: 36 36 577 240 gsave -35 35 541 183 boxprim clip newpath +35 35 542 205 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.5947 set_scale +0.6683 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font @@ -158,327 +158,321 @@ gsave 10 dict begin end grestore end grestore +% Command +gsave 10 dict begin +768 96 39 18 ellipse_path +stroke +gsave 10 dict begin +768 97 moveto (Command) 58 14.00 -0.50 alignedtext +end grestore +end grestore + +% Vernacinterp -> Command +newpath 675 166 moveto +681 163 688 159 692 156 curveto +706 147 725 131 742 118 curveto +stroke +newpath 740 117 moveto +749 112 lineto +743 120 lineto +closepath +gsave 0 setgray stroke grestore fill + % Himsg gsave 10 dict begin -757 205 29 18 ellipse_path +768 204 29 18 ellipse_path stroke gsave 10 dict begin -757 206 moveto (Himsg) 37 14.00 -0.50 alignedtext +768 205 moveto (Himsg) 37 14.00 -0.50 alignedtext end grestore end grestore % Vernacinterp -> Himsg -newpath 685 189 moveto -697 191 709 194 721 197 curveto +newpath 687 188 moveto +701 190 717 194 731 197 curveto stroke -newpath 721 194 moveto +newpath 731 194 moveto +740 199 lineto 730 199 lineto -720 199 lineto closepath gsave 0 setgray stroke grestore fill % Vernacentries gsave 10 dict begin -513 126 49 18 ellipse_path +513 97 49 18 ellipse_path stroke gsave 10 dict begin -513 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext +513 98 moveto (Vernacentries) 77 14.00 -0.50 alignedtext end grestore end grestore % Vernacentries -> Vernacinterp -newpath 546 139 moveto -563 146 586 155 604 163 curveto +newpath 536 113 moveto +554 127 581 145 598 156 curveto +601 158 603 159 607 161 curveto stroke -newpath 605 161 moveto -613 167 lineto -603 165 lineto +newpath 608 159 moveto +616 166 lineto +606 163 lineto closepath gsave 0 setgray stroke grestore fill -% Command +% Discharge gsave 10 dict begin -645 72 39 18 ellipse_path +645 126 38 18 ellipse_path stroke gsave 10 dict begin -645 73 moveto (Command) 58 14.00 -0.50 alignedtext +645 127 moveto (Discharge) 56 14.00 -0.50 alignedtext end grestore end grestore -% Vernacentries -> Command -newpath 546 113 moveto -564 105 588 96 607 88 curveto +% Vernacentries -> Discharge +newpath 555 106 moveto +570 109 586 113 601 116 curveto stroke -newpath 606 86 moveto -616 84 lineto -608 90 lineto +newpath 601 113 moveto +610 118 lineto +600 118 lineto closepath gsave 0 setgray stroke grestore fill -% Discharge +% Metasyntax gsave 10 dict begin -645 126 38 18 ellipse_path +645 72 43 18 ellipse_path stroke gsave 10 dict begin -645 127 moveto (Discharge) 56 14.00 -0.50 alignedtext +645 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext end grestore end grestore -% Vernacentries -> Discharge -newpath 562 126 moveto -574 126 585 126 596 126 curveto +% Vernacentries -> Metasyntax +newpath 557 89 moveto +570 87 583 84 596 81 curveto stroke -newpath 596 124 moveto -606 126 lineto -596 129 lineto +newpath 596 79 moveto +606 79 lineto +597 83 lineto closepath gsave 0 setgray stroke grestore fill -% Class +% Record gsave 10 dict begin -757 97 27 18 ellipse_path +645 18 30 18 ellipse_path stroke gsave 10 dict begin -757 98 moveto (Class) 30 14.00 -0.50 alignedtext +645 19 moveto (Record) 40 14.00 -0.50 alignedtext end grestore end grestore -% Discharge -> Class -newpath 679 117 moveto -693 114 709 110 723 106 curveto +% Vernacentries -> Record +newpath 537 81 moveto +556 69 582 52 598 42 curveto +602 39 609 36 615 33 curveto +stroke +newpath 611 32 moveto +621 30 lineto +613 37 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Record -> Command +newpath 669 29 moveto +677 34 686 38 692 42 curveto +706 51 724 63 739 75 curveto stroke -newpath 722 104 moveto -732 104 lineto -723 109 lineto +newpath 741 73 moveto +747 81 lineto +738 77 lineto closepath gsave 0 setgray stroke grestore fill % Vernac gsave 10 dict begin -513 180 30 18 ellipse_path +513 178 30 18 ellipse_path stroke gsave 10 dict begin -513 181 moveto (Vernac) 40 14.00 -0.50 alignedtext +513 179 moveto (Vernac) 40 14.00 -0.50 alignedtext end grestore end grestore % Vernac -> Vernacinterp -newpath 544 180 moveto -557 180 573 180 588 180 curveto +newpath 544 178 moveto +557 178 573 179 588 179 curveto stroke -newpath 588 178 moveto -598 180 lineto -588 183 lineto +newpath 588 177 moveto +598 179 lineto +588 182 lineto closepath gsave 0 setgray stroke grestore fill % Toplevel gsave 10 dict begin -239 234 35 18 ellipse_path +239 232 35 18 ellipse_path stroke gsave 10 dict begin -239 235 moveto (Toplevel) 49 14.00 -0.50 alignedtext +239 233 moveto (Toplevel) 49 14.00 -0.50 alignedtext end grestore end grestore % Mltop gsave 10 dict begin -369 261 27 18 ellipse_path +369 259 27 18 ellipse_path stroke gsave 10 dict begin -369 262 moveto (Mltop) 34 14.00 -0.50 alignedtext +369 260 moveto (Mltop) 34 14.00 -0.50 alignedtext end grestore end grestore % Toplevel -> Mltop -newpath 271 241 moveto -290 245 314 250 334 254 curveto +newpath 271 239 moveto +290 243 314 248 334 252 curveto stroke -newpath 334 251 moveto -343 256 lineto -333 256 lineto +newpath 334 249 moveto +343 254 lineto +333 254 lineto closepath gsave 0 setgray stroke grestore fill % Protectedtoplevel gsave 10 dict begin -369 207 59 18 ellipse_path +369 205 59 18 ellipse_path stroke gsave 10 dict begin -369 208 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext +369 206 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext end grestore end grestore % Toplevel -> Protectedtoplevel -newpath 271 227 moveto -283 225 297 222 310 219 curveto +newpath 271 225 moveto +283 223 297 220 310 217 curveto stroke -newpath 310 217 moveto -320 217 lineto -311 221 lineto +newpath 310 215 moveto +320 215 lineto +311 219 lineto closepath gsave 0 setgray stroke grestore fill % Protectedtoplevel -> Vernac -newpath 419 198 moveto -438 195 458 190 475 187 curveto +newpath 419 196 moveto +438 193 458 188 475 185 curveto stroke -newpath 474 185 moveto -484 186 lineto -474 190 lineto +newpath 474 183 moveto +484 184 lineto +474 188 lineto closepath gsave 0 setgray stroke grestore fill % Errors gsave 10 dict begin -513 234 27 18 ellipse_path +513 232 27 18 ellipse_path stroke gsave 10 dict begin -513 235 moveto (Errors) 34 14.00 -0.50 alignedtext +513 233 moveto (Errors) 34 14.00 -0.50 alignedtext end grestore end grestore % Protectedtoplevel -> Errors -newpath 419 216 moveto -439 219 460 224 478 227 curveto -stroke -newpath 477 224 moveto -486 229 lineto -476 229 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Record -gsave 10 dict begin -645 18 30 18 ellipse_path -stroke -gsave 10 dict begin -645 19 moveto (Record) 40 14.00 -0.50 alignedtext -end grestore -end grestore - -% Record -> Class -newpath 670 29 moveto -678 33 686 38 692 42 curveto -704 50 721 65 734 76 curveto -stroke -newpath 735 74 moveto -741 82 lineto -732 77 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Metasyntax -gsave 10 dict begin -865 97 43 18 ellipse_path -stroke -gsave 10 dict begin -865 98 moveto (Metasyntax) 65 14.00 -0.50 alignedtext -end grestore -end grestore - -% Class -> Metasyntax -newpath 784 97 moveto -792 97 802 97 812 97 curveto +newpath 419 214 moveto +439 217 460 222 478 225 curveto stroke -newpath 812 95 moveto -822 97 lineto -812 100 lineto +newpath 477 222 moveto +486 227 lineto +476 227 lineto closepath gsave 0 setgray stroke grestore fill % Errors -> Himsg -newpath 541 231 moveto -584 225 669 215 718 209 curveto +newpath 540 229 moveto +587 224 681 214 732 208 curveto stroke -newpath 718 207 moveto -728 208 lineto -718 211 lineto +newpath 729 206 moveto +739 207 lineto +729 211 lineto closepath gsave 0 setgray stroke grestore fill % Minicoq gsave 10 dict begin -34 288 34 18 ellipse_path +34 286 34 18 ellipse_path stroke gsave 10 dict begin -34 289 moveto (Minicoq) 47 14.00 -0.50 alignedtext +34 287 moveto (Minicoq) 47 14.00 -0.50 alignedtext end grestore end grestore % Fhimsg gsave 10 dict begin -136 288 31 18 ellipse_path +136 286 31 18 ellipse_path stroke gsave 10 dict begin -136 289 moveto (Fhimsg) 42 14.00 -0.50 alignedtext +136 287 moveto (Fhimsg) 42 14.00 -0.50 alignedtext end grestore end grestore % Minicoq -> Fhimsg -newpath 68 288 moveto -77 288 86 288 94 288 curveto +newpath 68 286 moveto +77 286 86 286 94 286 curveto stroke -newpath 94 286 moveto -104 288 lineto -94 291 lineto +newpath 94 284 moveto +104 286 lineto +94 289 lineto closepath gsave 0 setgray stroke grestore fill % Coqtop gsave 10 dict begin -34 207 31 18 ellipse_path +34 205 31 18 ellipse_path stroke gsave 10 dict begin -34 208 moveto (Coqtop) 41 14.00 -0.50 alignedtext +34 206 moveto (Coqtop) 41 14.00 -0.50 alignedtext end grestore end grestore % Coqinit gsave 10 dict begin -136 234 31 18 ellipse_path +136 232 31 18 ellipse_path stroke gsave 10 dict begin -136 235 moveto (Coqinit) 42 14.00 -0.50 alignedtext +136 233 moveto (Coqinit) 42 14.00 -0.50 alignedtext end grestore end grestore % Coqtop -> Coqinit -newpath 62 215 moveto -73 218 86 221 98 224 curveto +newpath 62 213 moveto +73 216 86 219 98 222 curveto stroke -newpath 98 221 moveto -107 227 lineto -97 226 lineto +newpath 98 219 moveto +107 225 lineto +97 224 lineto closepath gsave 0 setgray stroke grestore fill % Usage gsave 10 dict begin -136 180 27 18 ellipse_path +136 178 27 18 ellipse_path stroke gsave 10 dict begin -136 181 moveto (Usage) 34 14.00 -0.50 alignedtext +136 179 moveto (Usage) 34 14.00 -0.50 alignedtext end grestore end grestore % Coqtop -> Usage -newpath 62 199 moveto -74 196 88 192 101 189 curveto +newpath 62 197 moveto +74 194 88 190 101 187 curveto stroke -newpath 100 187 moveto -110 187 lineto -101 192 lineto +newpath 100 185 moveto +110 185 lineto +101 190 lineto closepath gsave 0 setgray stroke grestore fill % Coqinit -> Toplevel -newpath 168 234 moveto -176 234 185 234 194 234 curveto +newpath 168 232 moveto +176 232 185 232 194 232 curveto stroke -newpath 194 232 moveto -204 234 lineto -194 237 lineto +newpath 194 230 moveto +204 232 lineto +194 235 lineto closepath gsave 0 setgray stroke grestore fill endpage -- cgit v1.2.3