From e81fa5b551df4400bfd8af731a0440da30ba961b Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 16 May 2002 11:01:32 +0000 Subject: MAJ V7.3 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2699 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/parsing.dep.ps | 377 +++++++++++++++++++--------------------------- doc/pretyping.dep.ps | 417 +++++++++++++++++++++++++-------------------------- doc/toplevel.dep.ps | 22 +-- 3 files changed, 375 insertions(+), 441 deletions(-) (limited to 'doc') diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps index b3ca2ae16..9df862840 100644 --- a/doc/parsing.dep.ps +++ b/doc/parsing.dep.ps @@ -3,7 +3,7 @@ %%For: (herbelin) Hugo Herbelin %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 330 +%%BoundingBox: 36 36 576 232 %%EndComments %%BeginProlog save @@ -150,442 +150,379 @@ def %%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 330 +%%PageBoundingBox: 36 36 576 232 %%PageOrientation: Portrait gsave -35 35 541 295 boxprim clip newpath +35 35 541 197 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7479 set_scale +0.7584 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 576 330] /PAGES pdfmark +[ /CropBox [36 36 576 232] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Pcoq gsave 10 dict begin -591 251 27 18 ellipse_path +581 103 27 18 ellipse_path stroke gsave 10 dict begin -591 252 moveto (Pcoq) 28 14.00 -0.50 alignedtext +581 104 moveto (Pcoq) 28 14.00 -0.50 alignedtext end grestore end grestore % Coqast gsave 10 dict begin -684 251 30 18 ellipse_path +674 103 30 18 ellipse_path stroke gsave 10 dict begin -684 252 moveto (Coqast) 38 14.00 -0.50 alignedtext +674 104 moveto (Coqast) 38 14.00 -0.50 alignedtext end grestore end grestore % Pcoq -> Coqast -newpath 618 251 moveto -626 251 635 251 644 251 curveto +newpath 608 103 moveto +616 103 625 103 634 103 curveto stroke -newpath 644 249 moveto -654 251 lineto -644 254 lineto +newpath 634 101 moveto +644 103 lineto +634 106 lineto closepath gsave 0 setgray stroke grestore fill % Extend gsave 10 dict begin -405 224 30 18 ellipse_path +398 52 30 18 ellipse_path stroke gsave 10 dict begin -405 225 moveto (Extend) 39 14.00 -0.50 alignedtext +398 53 moveto (Extend) 39 14.00 -0.50 alignedtext end grestore end grestore % Ast gsave 10 dict begin -501 251 27 18 ellipse_path +491 103 27 18 ellipse_path stroke gsave 10 dict begin -501 252 moveto (Ast) 19 14.00 -0.50 alignedtext +491 104 moveto (Ast) 19 14.00 -0.50 alignedtext end grestore end grestore % Extend -> Ast -newpath 432 232 moveto -443 235 455 238 467 241 curveto +newpath 421 64 moveto +433 71 448 79 462 86 curveto stroke -newpath 467 238 moveto -476 244 lineto -466 243 lineto +newpath 463 84 moveto +470 91 lineto +460 88 lineto closepath gsave 0 setgray stroke grestore fill % Ast -> Pcoq -newpath 528 251 moveto -536 251 545 251 554 251 curveto +newpath 518 103 moveto +526 103 535 103 544 103 curveto stroke -newpath 554 249 moveto -564 251 lineto -554 254 lineto +newpath 544 101 moveto +554 103 lineto +544 106 lineto closepath gsave 0 setgray stroke grestore fill % Termast gsave 10 dict begin -405 278 33 18 ellipse_path +292 156 33 18 ellipse_path stroke gsave 10 dict begin -405 279 moveto (Termast) 45 14.00 -0.50 alignedtext +292 157 moveto (Termast) 45 14.00 -0.50 alignedtext end grestore end grestore % Termast -> Ast -newpath 435 270 moveto -445 267 456 264 467 261 curveto +newpath 325 152 moveto +355 149 401 143 428 136 curveto +438 133 451 127 462 120 curveto stroke -newpath 466 259 moveto -476 258 lineto -467 264 lineto +newpath 461 118 moveto +471 115 lineto +463 122 lineto closepath gsave 0 setgray stroke grestore fill % Search gsave 10 dict begin -39 305 29 18 ellipse_path +48 198 29 18 ellipse_path stroke gsave 10 dict begin -39 306 moveto (Search) 37 14.00 -0.50 alignedtext +48 199 moveto (Search) 37 14.00 -0.50 alignedtext end grestore end grestore % Astterm gsave 10 dict begin -296 170 33 18 ellipse_path +170 94 33 18 ellipse_path stroke gsave 10 dict begin -296 171 moveto (Astterm) 45 14.00 -0.50 alignedtext +170 95 moveto (Astterm) 45 14.00 -0.50 alignedtext end grestore end grestore % Search -> Astterm -newpath 61 293 moveto -65 289 69 285 70 281 curveto -90 199 63 103 106 32 curveto -126 0 190 10 220 32 curveto -252 57 237 111 256 146 curveto -258 149 260 151 263 153 curveto -stroke -newpath 264 151 moveto -272 157 lineto -262 155 lineto +newpath 71 186 moveto +78 183 84 178 88 174 curveto +104 157 109 133 124 118 curveto +127 115 132 112 137 109 curveto +stroke +newpath 134 108 moveto +144 106 lineto +136 112 lineto closepath gsave 0 setgray stroke grestore fill % Coqlib gsave 10 dict begin -296 374 29 18 ellipse_path +292 229 29 18 ellipse_path stroke gsave 10 dict begin -296 375 moveto (Coqlib) 38 14.00 -0.50 alignedtext +292 230 moveto (Coqlib) 38 14.00 -0.50 alignedtext end grestore end grestore % Search -> Coqlib -newpath 53 321 moveto -67 336 88 357 106 362 curveto -146 372 215 375 257 374 curveto +newpath 70 210 moveto +87 218 109 229 124 232 curveto +159 239 217 235 255 233 curveto stroke -newpath 256 372 moveto -266 374 lineto -256 377 lineto +newpath 253 231 moveto +263 232 lineto +253 236 lineto closepath gsave 0 setgray stroke grestore fill % Printer gsave 10 dict begin -163 278 29 18 ellipse_path +170 148 29 18 ellipse_path stroke gsave 10 dict begin -163 279 moveto (Printer) 38 14.00 -0.50 alignedtext +170 149 moveto (Printer) 38 14.00 -0.50 alignedtext end grestore end grestore % Search -> Printer -newpath 67 299 moveto -84 296 107 291 126 286 curveto +newpath 73 188 moveto +91 180 116 170 137 162 curveto stroke -newpath 125 284 moveto -135 284 lineto -126 289 lineto +newpath 135 160 moveto +145 158 lineto +137 165 lineto closepath gsave 0 setgray stroke grestore fill % Astterm -> Termast -newpath 321 182 moveto -327 186 333 190 336 194 curveto -352 211 358 235 372 254 curveto -374 256 376 258 378 260 curveto -stroke -newpath 377 256 moveto -384 264 lineto -374 261 lineto +newpath 194 106 moveto +213 116 239 129 260 139 curveto +stroke +newpath 260 136 moveto +268 143 lineto +258 141 lineto closepath gsave 0 setgray stroke grestore fill % Printer -> Termast -newpath 193 278 moveto -235 278 314 278 362 278 curveto +newpath 200 150 moveto +215 151 233 152 249 153 curveto stroke -newpath 362 276 moveto -372 278 lineto -362 281 lineto +newpath 249 151 moveto +259 154 lineto +249 155 lineto closepath gsave 0 setgray stroke grestore fill % Esyntax gsave 10 dict begin -296 224 33 18 ellipse_path +292 48 33 18 ellipse_path stroke gsave 10 dict begin -296 225 moveto (Esyntax) 45 14.00 -0.50 alignedtext +292 49 moveto (Esyntax) 45 14.00 -0.50 alignedtext end grestore end grestore % Printer -> Esyntax -newpath 188 268 moveto -208 259 237 247 260 238 curveto -stroke -newpath 259 236 moveto -269 235 lineto -260 241 lineto +newpath 194 137 moveto +203 133 211 128 216 124 curveto +232 109 238 86 252 72 curveto +254 70 256 68 259 66 curveto +stroke +newpath 258 64 moveto +268 61 lineto +260 68 lineto closepath gsave 0 setgray stroke grestore fill % Esyntax -> Extend -newpath 329 224 moveto -340 224 353 224 365 224 curveto +newpath 325 49 moveto +336 49 348 50 359 50 curveto stroke -newpath 365 222 moveto -375 224 lineto -365 227 lineto +newpath 358 47 moveto +368 51 lineto +358 52 lineto closepath gsave 0 setgray stroke grestore fill % Prettyp gsave 10 dict begin -39 251 30 18 ellipse_path +48 144 30 18 ellipse_path stroke gsave 10 dict begin -39 252 moveto (Prettyp) 40 14.00 -0.50 alignedtext +48 145 moveto (Prettyp) 40 14.00 -0.50 alignedtext end grestore end grestore % Prettyp -> Printer -newpath 68 257 moveto -85 260 107 265 126 270 curveto +newpath 78 145 moveto +94 146 114 146 131 147 curveto stroke -newpath 126 267 moveto -135 272 lineto -125 272 lineto +newpath 130 145 moveto +140 147 lineto +130 150 lineto closepath gsave 0 setgray stroke grestore fill % G_zsyntax gsave 10 dict begin -163 224 40 18 ellipse_path +48 86 40 18 ellipse_path stroke gsave 10 dict begin -163 225 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext +48 87 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext end grestore end grestore % G_zsyntax -> Astterm -newpath 193 212 moveto -213 204 240 193 261 184 curveto +newpath 88 89 moveto +101 90 115 91 128 91 curveto stroke -newpath 259 182 moveto -269 181 lineto -261 187 lineto +newpath 127 88 moveto +137 92 lineto +127 93 lineto closepath gsave 0 setgray stroke grestore fill % G_zsyntax -> Esyntax -newpath 203 224 moveto -219 224 237 224 254 224 curveto -stroke -newpath 253 222 moveto -263 224 lineto -253 227 lineto -closepath -gsave 0 setgray stroke grestore fill - -% G_string_syntax -gsave 10 dict begin -163 170 56 18 ellipse_path -stroke -gsave 10 dict begin -163 171 moveto (G_string_syntax) 92 14.00 -0.50 alignedtext -end grestore -end grestore - -% G_string_syntax -> Astterm -newpath 220 170 moveto -232 170 243 170 254 170 curveto -stroke -newpath 253 168 moveto -263 170 lineto -253 173 lineto -closepath -gsave 0 setgray stroke grestore fill - -% G_string_syntax -> Esyntax -newpath 198 184 moveto -217 192 242 202 261 210 curveto +newpath 80 75 moveto +95 71 112 66 124 64 curveto +159 58 214 54 251 51 curveto stroke -newpath 261 207 moveto -269 213 lineto -259 212 lineto +newpath 249 49 moveto +259 50 lineto +249 54 lineto closepath gsave 0 setgray stroke grestore fill % G_rsyntax gsave 10 dict begin -163 116 39 18 ellipse_path +48 25 39 18 ellipse_path stroke gsave 10 dict begin -163 117 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext +48 26 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext end grestore end grestore % G_rsyntax -> Astterm -newpath 193 128 moveto -213 136 240 147 261 156 curveto +newpath 73 39 moveto +92 50 119 65 139 77 curveto stroke -newpath 261 153 moveto -269 159 lineto -259 158 lineto +newpath 139 74 moveto +147 81 lineto +137 79 lineto closepath gsave 0 setgray stroke grestore fill % G_rsyntax -> Esyntax -newpath 192 128 moveto -206 134 220 140 220 140 curveto -238 155 241 182 256 200 curveto -258 202 260 204 263 206 curveto -stroke -newpath 264 204 moveto -272 211 lineto -262 208 lineto +newpath 88 26 moveto +126 26 182 28 216 31 curveto +226 32 242 35 255 38 curveto +stroke +newpath 253 35 moveto +262 40 lineto +252 40 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax gsave 10 dict begin -163 332 45 18 ellipse_path +170 202 45 18 ellipse_path stroke gsave 10 dict begin -163 333 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext +170 203 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext end grestore end grestore % G_natsyntax -> Termast -newpath 203 323 moveto -248 313 320 297 365 287 curveto +newpath 203 190 moveto +219 184 239 176 256 169 curveto stroke -newpath 364 285 moveto -374 285 lineto -365 290 lineto +newpath 255 167 moveto +265 166 lineto +256 172 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax -> Coqlib -newpath 199 343 moveto -218 349 242 357 261 363 curveto +newpath 210 211 moveto +225 214 241 218 255 221 curveto stroke -newpath 261 360 moveto -270 366 lineto -260 365 lineto +newpath 255 218 moveto +264 223 lineto +254 223 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax -> Esyntax -newpath 197 320 moveto -206 316 214 312 220 308 curveto -238 294 261 267 277 248 curveto -stroke -newpath 275 247 moveto -283 241 lineto -278 250 lineto -closepath -gsave 0 setgray stroke grestore fill - -% G_ascii_syntax -gsave 10 dict begin -163 62 53 18 ellipse_path -stroke -gsave 10 dict begin -163 63 moveto (G_ascii_syntax) 86 14.00 -0.50 alignedtext -end grestore -end grestore - -% G_ascii_syntax -> Astterm -newpath 201 75 moveto -209 78 216 82 220 86 curveto -238 101 241 128 256 146 curveto -258 148 260 150 263 152 curveto -stroke -newpath 264 150 moveto -272 157 lineto -262 154 lineto -closepath -gsave 0 setgray stroke grestore fill - -% G_ascii_syntax -> Esyntax -newpath 203 74 moveto -210 77 216 80 220 86 curveto -243 119 237 165 256 200 curveto -258 203 260 205 263 207 curveto -stroke -newpath 264 205 moveto -272 211 lineto -262 209 lineto +newpath 201 189 moveto +207 186 213 183 216 178 curveto +236 146 234 104 252 72 curveto +252 72 256 70 261 66 curveto +stroke +newpath 260 64 moveto +270 61 lineto +262 68 lineto closepath gsave 0 setgray stroke grestore fill % Egrammar gsave 10 dict begin -296 116 40 18 ellipse_path +292 102 40 18 ellipse_path stroke gsave 10 dict begin -296 117 moveto (Egrammar) 58 14.00 -0.50 alignedtext +292 103 moveto (Egrammar) 58 14.00 -0.50 alignedtext end grestore end grestore % Egrammar -> Extend -newpath 320 131 moveto -329 136 336 140 336 140 curveto -351 155 372 181 388 201 curveto +newpath 320 89 moveto +334 82 351 74 366 67 curveto stroke -newpath 389 198 moveto -393 208 lineto -385 201 lineto +newpath 364 65 moveto +374 63 lineto +366 70 lineto closepath gsave 0 setgray stroke grestore fill % Lexer gsave 10 dict begin -405 116 27 18 ellipse_path +398 106 27 18 ellipse_path stroke gsave 10 dict begin -405 117 moveto (Lexer) 32 14.00 -0.50 alignedtext +398 107 moveto (Lexer) 32 14.00 -0.50 alignedtext end grestore end grestore % Egrammar -> Lexer -newpath 336 116 moveto -347 116 358 116 368 116 curveto +newpath 332 104 moveto +342 104 352 105 361 105 curveto stroke -newpath 368 114 moveto -378 116 lineto -368 119 lineto +newpath 361 103 moveto +371 105 lineto +361 108 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps index 8af063428..e6a242ac4 100644 --- a/doc/pretyping.dep.ps +++ b/doc/pretyping.dep.ps @@ -3,7 +3,7 @@ %%For: (herbelin) Hugo Herbelin %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 577 203 +%%BoundingBox: 36 36 577 201 %%EndComments %%BeginProlog save @@ -150,439 +150,439 @@ def %%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 577 203 +%%PageBoundingBox: 36 36 577 201 %%PageOrientation: Portrait gsave -35 35 542 168 boxprim clip newpath +35 35 542 166 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0.4796 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 577 203] /PAGES pdfmark +[ /CropBox [36 36 577 201] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Multcase gsave 10 dict begin -355 234 36 18 ellipse_path +355 272 36 18 ellipse_path stroke gsave 10 dict begin -355 235 moveto (Multcase) 51 14.00 -0.50 alignedtext +355 273 moveto (Multcase) 51 14.00 -0.50 alignedtext end grestore end grestore % Evarutil gsave 10 dict begin -468 234 33 18 ellipse_path +468 272 33 18 ellipse_path stroke gsave 10 dict begin -468 235 moveto (Evarutil) 45 14.00 -0.50 alignedtext +468 273 moveto (Evarutil) 45 14.00 -0.50 alignedtext end grestore end grestore % Multcase -> Evarutil -newpath 391 234 moveto -402 234 414 234 425 234 curveto +newpath 391 272 moveto +402 272 414 272 425 272 curveto stroke -newpath 425 232 moveto -435 234 lineto -425 237 lineto +newpath 425 270 moveto +435 272 lineto +425 275 lineto closepath gsave 0 setgray stroke grestore fill % Pretype_errors gsave 10 dict begin -596 180 51 18 ellipse_path +596 272 51 18 ellipse_path stroke gsave 10 dict begin -596 181 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext +596 273 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext end grestore end grestore % Evarutil -> Pretype_errors -newpath 494 223 moveto -511 216 535 206 554 198 curveto +newpath 501 272 moveto +511 272 523 272 534 272 curveto stroke -newpath 553 196 moveto -563 194 lineto -555 200 lineto +newpath 534 270 moveto +544 272 lineto +534 275 lineto closepath gsave 0 setgray stroke grestore fill % Indrec gsave 10 dict begin -596 288 28 18 ellipse_path +596 326 28 18 ellipse_path stroke gsave 10 dict begin -596 289 moveto (Indrec) 35 14.00 -0.50 alignedtext +596 327 moveto (Indrec) 35 14.00 -0.50 alignedtext end grestore end grestore % Evarutil -> Indrec -newpath 494 245 moveto -514 254 542 266 564 275 curveto +newpath 494 283 moveto +514 292 542 304 564 313 curveto stroke -newpath 564 272 moveto -572 278 lineto -562 277 lineto +newpath 564 310 moveto +572 316 lineto +562 315 lineto closepath gsave 0 setgray stroke grestore fill % Typing gsave 10 dict begin -468 180 30 18 ellipse_path +468 218 30 18 ellipse_path stroke gsave 10 dict begin -468 181 moveto (Typing) 40 14.00 -0.50 alignedtext +468 219 moveto (Typing) 40 14.00 -0.50 alignedtext end grestore end grestore % Typing -> Pretype_errors -newpath 499 180 moveto -510 180 522 180 534 180 curveto +newpath 493 229 moveto +510 236 534 246 554 254 curveto stroke -newpath 534 178 moveto -544 180 lineto -534 183 lineto +newpath 555 252 moveto +563 258 lineto +553 256 lineto closepath gsave 0 setgray stroke grestore fill % Rawterm gsave 10 dict begin -731 126 36 18 ellipse_path +731 164 36 18 ellipse_path stroke gsave 10 dict begin -731 127 moveto (Rawterm) 51 14.00 -0.50 alignedtext +731 165 moveto (Rawterm) 51 14.00 -0.50 alignedtext end grestore end grestore % Pretype_errors -> Rawterm -newpath 630 166 moveto -649 158 674 149 694 141 curveto +newpath 630 258 moveto +637 255 644 251 648 248 curveto +667 233 692 206 710 187 curveto stroke -newpath 692 139 moveto -702 137 lineto -694 144 lineto +newpath 708 186 moveto +716 180 lineto +711 189 lineto closepath gsave 0 setgray stroke grestore fill % Inductiveops gsave 10 dict begin -731 180 46 18 ellipse_path +731 245 46 18 ellipse_path stroke gsave 10 dict begin -731 181 moveto (Inductiveops) 72 14.00 -0.50 alignedtext +731 246 moveto (Inductiveops) 72 14.00 -0.50 alignedtext end grestore end grestore % Pretype_errors -> Inductiveops -newpath 648 180 moveto -657 180 665 180 674 180 curveto +newpath 641 263 moveto +654 261 667 258 680 255 curveto stroke -newpath 674 178 moveto -684 180 lineto -674 183 lineto +newpath 679 253 moveto +689 253 lineto +680 258 lineto closepath gsave 0 setgray stroke grestore fill % Tacred gsave 10 dict begin -731 34 29 18 ellipse_path +731 56 29 18 ellipse_path stroke gsave 10 dict begin -731 35 moveto (Tacred) 38 14.00 -0.50 alignedtext +731 57 moveto (Tacred) 38 14.00 -0.50 alignedtext end grestore end grestore % Cbv gsave 10 dict begin -863 46 27 18 ellipse_path +863 56 27 18 ellipse_path stroke gsave 10 dict begin -863 47 moveto (Cbv) 23 14.00 -0.50 alignedtext +863 57 moveto (Cbv) 23 14.00 -0.50 alignedtext end grestore end grestore % Tacred -> Cbv -newpath 760 37 moveto -780 39 806 41 827 43 curveto +newpath 761 56 moveto +781 56 806 56 827 56 curveto stroke -newpath 826 40 moveto -836 44 lineto -826 45 lineto +newpath 826 54 moveto +836 56 lineto +826 59 lineto closepath gsave 0 setgray stroke grestore fill % Reductionops gsave 10 dict begin -863 134 49 18 ellipse_path +863 110 49 18 ellipse_path stroke gsave 10 dict begin -863 135 moveto (Reductionops) 77 14.00 -0.50 alignedtext +863 111 moveto (Reductionops) 77 14.00 -0.50 alignedtext end grestore end grestore % Tacred -> Reductionops -newpath 752 47 moveto -764 55 778 63 778 63 curveto -795 75 819 96 837 111 curveto +newpath 756 66 moveto +774 74 800 84 821 92 curveto stroke -newpath 838 109 moveto -844 117 lineto -835 112 lineto +newpath 822 90 moveto +830 96 lineto +820 94 lineto closepath gsave 0 setgray stroke grestore fill % Instantiate gsave 10 dict begin -988 57 39 18 ellipse_path +988 56 39 18 ellipse_path stroke gsave 10 dict begin -988 58 moveto (Instantiate) 58 14.00 -0.50 alignedtext +988 57 moveto (Instantiate) 58 14.00 -0.50 alignedtext end grestore end grestore % Cbv -> Instantiate -newpath 890 48 moveto -904 50 922 51 939 53 curveto +newpath 890 56 moveto +904 56 922 56 938 56 curveto stroke -newpath 939 51 moveto -949 54 lineto -939 55 lineto +newpath 938 54 moveto +948 56 lineto +938 59 lineto closepath gsave 0 setgray stroke grestore fill % Reductionops -> Instantiate -newpath 888 118 moveto -908 106 936 89 957 77 curveto +newpath 895 96 moveto +912 88 933 80 951 72 curveto stroke -newpath 954 76 moveto -964 72 lineto -957 80 lineto +newpath 949 70 moveto +959 68 lineto +951 75 lineto closepath gsave 0 setgray stroke grestore fill % Termops gsave 10 dict begin -988 134 35 18 ellipse_path +988 110 35 18 ellipse_path stroke gsave 10 dict begin -988 135 moveto (Termops) 49 14.00 -0.50 alignedtext +988 111 moveto (Termops) 49 14.00 -0.50 alignedtext end grestore end grestore % Reductionops -> Termops -newpath 912 134 moveto -923 134 933 134 943 134 curveto +newpath 912 110 moveto +923 110 933 110 943 110 curveto stroke -newpath 943 132 moveto -953 134 lineto -943 137 lineto +newpath 943 108 moveto +953 110 lineto +943 113 lineto closepath gsave 0 setgray stroke grestore fill % Syntax_def gsave 10 dict begin -596 126 42 18 ellipse_path +596 164 42 18 ellipse_path stroke gsave 10 dict begin -596 127 moveto (Syntax_def) 63 14.00 -0.50 alignedtext +596 165 moveto (Syntax_def) 63 14.00 -0.50 alignedtext end grestore end grestore % Syntax_def -> Rawterm -newpath 638 126 moveto -653 126 670 126 685 126 curveto +newpath 638 164 moveto +653 164 670 164 685 164 curveto stroke -newpath 685 124 moveto -695 126 lineto -685 129 lineto +newpath 685 162 moveto +695 164 lineto +685 167 lineto closepath gsave 0 setgray stroke grestore fill % Retyping gsave 10 dict begin -355 311 36 18 ellipse_path +355 49 36 18 ellipse_path stroke gsave 10 dict begin -355 312 moveto (Retyping) 51 14.00 -0.50 alignedtext +355 50 moveto (Retyping) 51 14.00 -0.50 alignedtext end grestore end grestore % Retyping -> Reductionops -newpath 388 318 moveto -450 329 582 348 648 318 curveto -713 288 802 199 842 157 curveto -stroke -newpath 839 157 moveto -847 151 lineto -843 160 lineto +newpath 389 43 moveto +469 30 670 2 778 26 curveto +801 31 798 69 814 86 curveto +817 89 820 91 824 92 curveto +stroke +newpath 825 90 moveto +833 96 lineto +823 94 lineto closepath gsave 0 setgray stroke grestore fill % Evd gsave 10 dict begin -1091 57 27 18 ellipse_path +1091 56 27 18 ellipse_path stroke gsave 10 dict begin -1091 58 moveto (Evd) 22 14.00 -0.50 alignedtext +1091 57 moveto (Evd) 22 14.00 -0.50 alignedtext end grestore end grestore % Instantiate -> Evd -newpath 1028 57 moveto -1037 57 1046 57 1054 57 curveto +newpath 1028 56 moveto +1037 56 1046 56 1054 56 curveto stroke -newpath 1054 55 moveto -1064 57 lineto -1054 60 lineto +newpath 1054 54 moveto +1064 56 lineto +1054 59 lineto closepath gsave 0 setgray stroke grestore fill % Recordops gsave 10 dict begin -468 72 40 18 ellipse_path +468 110 40 18 ellipse_path stroke gsave 10 dict begin -468 73 moveto (Recordops) 59 14.00 -0.50 alignedtext +468 111 moveto (Recordops) 59 14.00 -0.50 alignedtext end grestore end grestore % Classops gsave 10 dict begin -596 18 35 18 ellipse_path +596 56 35 18 ellipse_path stroke gsave 10 dict begin -596 19 moveto (Classops) 49 14.00 -0.50 alignedtext +596 57 moveto (Classops) 49 14.00 -0.50 alignedtext end grestore end grestore % Recordops -> Classops -newpath 497 60 moveto -516 52 541 41 561 33 curveto +newpath 497 98 moveto +516 90 541 79 561 71 curveto stroke -newpath 559 31 moveto -569 30 lineto -561 36 lineto +newpath 559 69 moveto +569 68 lineto +561 74 lineto closepath gsave 0 setgray stroke grestore fill % Classops -> Tacred -newpath 630 22 moveto -649 25 673 27 693 30 curveto +newpath 631 56 moveto +650 56 673 56 692 56 curveto stroke -newpath 692 27 moveto -702 31 lineto -692 32 lineto +newpath 691 54 moveto +701 56 lineto +691 59 lineto closepath gsave 0 setgray stroke grestore fill % Classops -> Rawterm -newpath 622 30 moveto -635 36 648 42 648 42 curveto -667 56 692 83 710 103 curveto +newpath 622 68 moveto +635 74 648 80 648 80 curveto +667 94 692 121 710 141 curveto stroke -newpath 711 100 moveto -716 109 lineto -707 104 lineto +newpath 711 138 moveto +716 147 lineto +707 142 lineto closepath gsave 0 setgray stroke grestore fill % Pretyping gsave 10 dict begin -46 245 37 18 ellipse_path +46 114 37 18 ellipse_path stroke gsave 10 dict begin -46 246 moveto (Pretyping) 54 14.00 -0.50 alignedtext +46 115 moveto (Pretyping) 54 14.00 -0.50 alignedtext end grestore end grestore % Cases gsave 10 dict begin -147 245 27 18 ellipse_path +147 114 27 18 ellipse_path stroke gsave 10 dict begin -147 246 moveto (Cases) 32 14.00 -0.50 alignedtext +147 115 moveto (Cases) 32 14.00 -0.50 alignedtext end grestore end grestore % Pretyping -> Cases -newpath 84 245 moveto -93 245 102 245 110 245 curveto +newpath 84 114 moveto +93 114 102 114 110 114 curveto stroke -newpath 110 243 moveto -120 245 lineto -110 248 lineto +newpath 110 112 moveto +120 114 lineto +110 117 lineto closepath gsave 0 setgray stroke grestore fill % Coercion gsave 10 dict begin -246 245 36 18 ellipse_path +246 114 36 18 ellipse_path stroke gsave 10 dict begin -246 246 moveto (Coercion) 51 14.00 -0.50 alignedtext +246 115 moveto (Coercion) 51 14.00 -0.50 alignedtext end grestore end grestore % Cases -> Coercion -newpath 174 245 moveto -182 245 191 245 200 245 curveto +newpath 174 114 moveto +182 114 191 114 200 114 curveto stroke -newpath 200 243 moveto -210 245 lineto -200 248 lineto +newpath 200 112 moveto +210 114 lineto +200 117 lineto closepath gsave 0 setgray stroke grestore fill % Inductiveops -> Reductionops -newpath 766 168 moveto -782 162 801 155 818 149 curveto +newpath 748 228 moveto +771 204 815 159 841 132 curveto stroke -newpath 817 147 moveto -827 146 lineto -818 152 lineto +newpath 837 132 moveto +846 127 lineto +841 136 lineto closepath gsave 0 setgray stroke grestore fill % Pattern gsave 10 dict begin -596 72 30 18 ellipse_path +596 110 30 18 ellipse_path stroke gsave 10 dict begin -596 73 moveto (Pattern) 39 14.00 -0.50 alignedtext +596 111 moveto (Pattern) 39 14.00 -0.50 alignedtext end grestore end grestore % Pattern -> Reductionops -newpath 626 75 moveto -666 79 737 86 778 96 curveto -785 98 806 107 826 117 curveto +newpath 626 110 moveto +670 110 751 110 806 110 curveto stroke -newpath 825 114 moveto -833 120 lineto -823 118 lineto +newpath 804 108 moveto +814 110 lineto +804 113 lineto closepath gsave 0 setgray stroke grestore fill % Pattern -> Rawterm -newpath 621 82 moveto -641 91 671 102 694 112 curveto +newpath 621 120 moveto +641 129 671 140 694 150 curveto stroke -newpath 694 109 moveto -703 115 lineto -693 114 lineto +newpath 694 147 moveto +703 153 lineto +693 152 lineto closepath gsave 0 setgray stroke grestore fill % Indrec -> Inductiveops -newpath 620 279 moveto -631 274 642 269 648 264 curveto -666 250 692 223 710 204 curveto +newpath 619 316 moveto +630 311 641 306 648 302 curveto +663 293 683 279 700 267 curveto stroke -newpath 708 203 moveto -716 197 lineto -711 206 lineto +newpath 699 265 moveto +708 261 lineto +702 269 lineto closepath gsave 0 setgray stroke grestore fill @@ -596,85 +596,82 @@ end grestore end grestore % Evarconv -> Evarutil -newpath 381 193 moveto -397 201 418 211 435 218 curveto +newpath 372 196 moveto +388 212 412 235 428 248 curveto +431 250 433 251 436 253 curveto stroke -newpath 435 215 moveto -443 222 lineto -433 220 lineto +newpath 438 251 moveto +445 259 lineto +435 256 lineto closepath gsave 0 setgray stroke grestore fill % Evarconv -> Typing -newpath 392 180 moveto -404 180 416 180 427 180 curveto +newpath 386 190 moveto +400 195 418 201 432 206 curveto stroke -newpath 427 178 moveto -437 180 lineto -427 183 lineto +newpath 432 203 moveto +441 209 lineto +431 208 lineto closepath gsave 0 setgray stroke grestore fill % Evarconv -> Recordops -newpath 372 164 moveto -391 145 422 116 444 95 curveto +newpath 378 166 moveto +395 156 418 141 436 130 curveto stroke -newpath 442 93 moveto -451 88 lineto -446 97 lineto +newpath 434 128 moveto +444 125 lineto +437 132 lineto closepath gsave 0 setgray stroke grestore fill % Detyping gsave 10 dict begin -596 234 36 18 ellipse_path +596 218 36 18 ellipse_path stroke gsave 10 dict begin -596 235 moveto (Detyping) 52 14.00 -0.50 alignedtext +596 219 moveto (Detyping) 52 14.00 -0.50 alignedtext end grestore end grestore % Detyping -> Rawterm -newpath 626 223 moveto -634 220 643 215 648 210 curveto -665 193 668 166 684 150 curveto -684 150 689 147 697 144 curveto -stroke -newpath 696 142 moveto -706 139 lineto -698 146 lineto +newpath 625 207 moveto +645 199 673 188 694 179 curveto +stroke +newpath 693 177 moveto +703 175 lineto +695 181 lineto closepath gsave 0 setgray stroke grestore fill -% Detyping -> Termops -newpath 632 230 moveto -673 226 739 219 778 210 curveto -825 199 868 180 912 164 curveto -912 164 932 156 951 149 curveto +% Detyping -> Inductiveops +newpath 630 225 moveto +645 228 663 232 679 235 curveto stroke -newpath 950 147 moveto -960 145 lineto -952 151 lineto +newpath 680 233 moveto +689 237 lineto +679 237 lineto closepath gsave 0 setgray stroke grestore fill % Coercion -> Retyping -newpath 269 259 moveto -285 269 306 282 324 292 curveto +newpath 269 100 moveto +285 91 306 78 323 68 curveto stroke -newpath 325 290 moveto -332 297 lineto -322 294 lineto +newpath 321 66 moveto +331 63 lineto +324 70 lineto closepath gsave 0 setgray stroke grestore fill % Coercion -> Evarconv -newpath 269 231 moveto -285 222 306 209 323 199 curveto +newpath 269 128 moveto +285 138 306 151 324 161 curveto stroke -newpath 321 197 moveto -331 194 lineto -324 201 lineto +newpath 325 159 moveto +332 166 lineto +322 163 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps index d05a3aba8..9679cb66f 100644 --- a/doc/toplevel.dep.ps +++ b/doc/toplevel.dep.ps @@ -431,22 +431,22 @@ newpath 502 117 moveto closepath gsave 0 setgray stroke grestore fill -% Errors +% Cerrors gsave 10 dict begin -542 72 27 18 ellipse_path +542 72 31 18 ellipse_path stroke gsave 10 dict begin -542 73 moveto (Errors) 34 14.00 -0.50 alignedtext +542 73 moveto (Cerrors) 41 14.00 -0.50 alignedtext end grestore end grestore -% Protectedtoplevel -> Errors +% Protectedtoplevel -> Cerrors newpath 429 90 moveto -455 86 484 81 507 78 curveto +454 86 481 82 503 78 curveto stroke -newpath 505 76 moveto -515 77 lineto -505 81 lineto +newpath 502 76 moveto +512 77 lineto +502 81 lineto closepath gsave 0 setgray stroke grestore fill @@ -470,9 +470,9 @@ newpath 488 32 moveto closepath gsave 0 setgray stroke grestore fill -% Errors -> Himsg -newpath 570 73 moveto -620 74 725 76 781 77 curveto +% Cerrors -> Himsg +newpath 573 73 moveto +625 74 726 76 782 77 curveto stroke newpath 779 75 moveto 789 77 lineto -- cgit v1.2.3