From 777a06c8b165f245a064e188c4da3739bd555cc7 Mon Sep 17 00:00:00 2001 From: filliatr Date: Mon, 3 Feb 2003 08:33:29 +0000 Subject: release 7.4; changement magic number git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3652 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ANNONCE | 11 +- CHANGES | 4 +- INSTALL | 14 +- README | 4 +- README.win | 3 +- distrib/RH/coq.spec.tpl | 6 +- doc/kernel.dep.ps | 596 ++++++++++++++++++++++++++++----------- doc/library.dep.ps | 467 ++++++++++++++++++++----------- doc/parsing.dep.ps | 635 ++++++++++++++++++++++++++---------------- doc/pretyping.dep.ps | 719 +++++++++++++++++++++++++++--------------------- doc/proofs.dep.ps | 345 ++++++++++++++--------- doc/tactics.dep.ps | 582 +++++++++++++++++++++++---------------- doc/toplevel.dep.ps | 585 ++++++++++++++++++++++++--------------- library/library.ml | 2 +- 14 files changed, 2503 insertions(+), 1470 deletions(-) diff --git a/ANNONCE b/ANNONCE index df11742c6..c7a23cf1d 100644 --- a/ANNONCE +++ b/ANNONCE @@ -1,14 +1,14 @@ - The Coq development team is pleased to announce the release of Coq +The Coq development team is pleased to announce the release of Coq version 7.4. -This is not a major release, the main purpose this version is to offer + This is not a major release; the main purpose of this version is to offer novelties (including the module system) required by the Why (http://why.lri.fr) and Krakatoa (http://www.lri.fr/~marche/krakatoa) systems. See file CHANGES for a detailed list of changes, novelties, bug-fixes and incompatibilities. - Coq V7.4 is available in several formats from http://coq.inria.fr -and ftp://ftp.inria.fr/INRIA/coq/V7.4. + Coq V7.4 is available in several formats from http://coq.inria.fr/ +and ftp://ftp.inria.fr/INRIA/coq/V7.4/ The documentation is available in postscript, pdf and html format. @@ -20,8 +20,7 @@ by coqdoc). ftp://ftp.inria.fr/INRIA/coq/V7.4/doc/Changes.html for a full list of changes including sources of incompatibilities. - Users are kindly invited to report bugs at - http://coq.inria.fr/bin/coq-bugs + Users are kindly invited to report bugs at http://coq.inria.fr/bin/coq-bugs and to mail Coq-Club@pauillac.inria.fr for general questions or remarks. Note that you can now choose your personal options at http://pauillac.inria.fr/mailman/listinfo/coq-club and consult the diff --git a/CHANGES b/CHANGES index 20923b99c..f773620b6 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,5 @@ Changes from V7.3.1 to V7.4 ---------------------------- +=========================== Grammar extension @@ -177,7 +177,7 @@ Misc LetTac (PR#192) Changes from V7.2 to V7.3 -------------------------- +========================= Language diff --git a/INSTALL b/INSTALL index bdd9ee43e..72c4d2fdc 100644 --- a/INSTALL +++ b/INSTALL @@ -1,19 +1,16 @@ - INSTALLATION PROCEDURES FOR THE COQ V7.3 SYSTEM + INSTALLATION PROCEDURES FOR THE COQ V7.4 SYSTEM ----------------------------------------------- WHAT DO YOU NEED ? ================== Coq is designed to work on computers equipped with the Unix operating - system. In order to compile Coq V7.3 you need: + system. In order to compile Coq V7.4 you need: - - Objective Caml version 3.01 or later + - Objective Caml version 3.06 or later (available at http://caml.inria.fr/) - - the Camlp4 preprocessor with same version number as ocaml - (available at http://caml.inria.fr/camlp4/) - Until now, it has mainly been tested on Sun workstations running Solaris, and DEC alpha and Pentium workstations running Linux. By FTP, Coq comes as a single compressed tar-file. You have probably already @@ -32,7 +29,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.01 (or later) +1- Check that you have the Objective Caml compiler version 3.06 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. @@ -48,6 +45,9 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). (You need Camlp4 in both bytecode and native versions if your platform supports it). + Note: in the latest ocaml distributions, camlp4 comes with ocaml so + you do not have to check this point anymore. + 3- The uncompression and un-tarring of the distribution file gave birth to a directory named "coq-7.xx". You can rename this directory and put it wherever you want. Just keep in mind that you will need some spare diff --git a/README b/README index ed9a386c3..eb99ec631 100644 --- a/README +++ b/README @@ -1,5 +1,5 @@ - THE COQ V7.3 SYSTEM + THE COQ V7.4 SYSTEM =================== INSTALLATION. @@ -11,7 +11,7 @@ INSTALLATION. DOCUMENTATION. ============== - The documentation of Coq V7.3 is available by anonymous ftp (see below), + The documentation of Coq V7.4 is available by anonymous ftp (see below), in a directory doc/. The documents are available separately or all together in the tar file all-docs.tar . diff --git a/README.win b/README.win index 9716d49ac..b1054c97d 100644 --- a/README.win +++ b/README.win @@ -15,8 +15,7 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml version 3.01 or later and camlp4 with same - version number as ocaml (but at least 3.01.6), Visual C++ (needed + 1- Install ocaml version 3.06 or later, Visual C++ (needed for the -custom option of ocaml) and MASM (needed if you want to produce a native version). diff --git a/distrib/RH/coq.spec.tpl b/distrib/RH/coq.spec.tpl index 6266e4f66..57c7af35d 100644 --- a/distrib/RH/coq.spec.tpl +++ b/distrib/RH/coq.spec.tpl @@ -1,12 +1,12 @@ Name: coq -Version: 7.3 +Version: 7.4 Release: 1 Summary: The Coq Proof Assistant Copyright: freely redistributable Group: Applications/Math Vendor: INRIA Rocquencourt URL: http://coq.inria.fr -Source: ftp://ftp.inria.fr/INRIA/coq/V7.3/coq-7.3.tar.gz +Source: ftp://ftp.inria.fr/INRIA/coq/V7.4/coq-7.4.tar.gz Icon: petit-coq.gif %description @@ -19,7 +19,7 @@ Coq is a proof assistant which: # Ocaml is required but it is better to install it not with rpm but by # hand in /usr/local -# Requires: ocaml >= 3.01 +# Requires: ocaml >= 3.06 %prep diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps index e707a62c8..a0be6b4ca 100644 --- a/doc/kernel.dep.ps +++ b/doc/kernel.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (herbelin) Hugo Herbelin +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 70 +%%BoundingBox: 35 35 577 88 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,324 +225,516 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 70 +%%PageBoundingBox: 36 36 577 88 %%PageOrientation: Portrait gsave -35 35 541 35 boxprim clip newpath +35 35 542 53 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.3614 set_scale +0.2736 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 576 70] /PAGES pdfmark +[ /CropBox [36 36 577 88] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Univ gsave 10 dict begin -1361 74 27 18 ellipse_path +1826 172 28 18 ellipse_path stroke gsave 10 dict begin -1361 75 moveto (Univ) 28 14.00 -0.50 alignedtext +1826 167 moveto 35 -0.5 (Univ) alignedtext end grestore end grestore % Names gsave 10 dict begin -1456 74 29 18 ellipse_path +1931 172 35 18 ellipse_path stroke gsave 10 dict begin -1456 75 moveto (Names) 38 14.00 -0.50 alignedtext +1931 167 moveto 48 -0.5 (Names) alignedtext end grestore end grestore % Univ -> Names -newpath 1388 74 moveto -1397 74 1407 74 1416 74 curveto +newpath 1855 172 moveto +1865 172 1875 172 1886 172 curveto stroke -newpath 1416 72 moveto -1426 74 lineto -1416 77 lineto +0.000 0.000 0.000 edgecolor +newpath 1886 170 moveto +1896 172 lineto +1886 175 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Typeops gsave 10 dict begin -273 18 34 18 ellipse_path +613 149 40 18 ellipse_path stroke gsave 10 dict begin -273 19 moveto (Typeops) 48 14.00 -0.50 alignedtext +613 144 moveto 58 -0.5 (Typeops) alignedtext end grestore end grestore +% Entries +gsave 10 dict begin +872 168 35 18 ellipse_path +stroke +gsave 10 dict begin +872 163 moveto 48 -0.5 (Entries) alignedtext +end grestore +end grestore + +% Typeops -> Entries +newpath 653 152 moveto +701 155 781 161 830 165 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 827 163 moveto +837 165 lineto +827 168 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + % Inductive gsave 10 dict begin -381 20 36 18 ellipse_path +739 72 43 18 ellipse_path stroke gsave 10 dict begin -381 21 moveto (Inductive) 52 14.00 -0.50 alignedtext +739 67 moveto 64 -0.5 (Inductive) alignedtext end grestore end grestore % Typeops -> Inductive -newpath 308 19 moveto -317 19 326 19 334 19 curveto +newpath 637 134 moveto +657 122 685 105 706 92 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 704 90 moveto +714 87 lineto +707 94 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Sign +gsave 10 dict begin +1633 145 27 18 ellipse_path stroke -newpath 334 17 moveto -344 19 lineto -334 22 lineto +gsave 10 dict begin +1633 140 moveto 30 -0.5 (Sign) alignedtext +end grestore +end grestore + +% Entries -> Sign +newpath 907 168 moveto +976 168 1124 167 1147 168 curveto +1147 168 1147 168 1387 168 curveto +1462 167 1549 157 1597 150 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1597 148 moveto +1607 149 lineto +1597 152 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Type_errors gsave 10 dict begin -499 24 44 18 ellipse_path +872 72 53 18 ellipse_path stroke gsave 10 dict begin -499 25 moveto (Type_errors) 68 14.00 -0.50 alignedtext +872 67 moveto 85 -0.5 (Type_errors) alignedtext end grestore end grestore % Inductive -> Type_errors -newpath 418 21 moveto -426 21 435 22 444 22 curveto +newpath 782 72 moveto +791 72 799 72 808 72 curveto stroke -newpath 444 20 moveto -454 22 lineto -444 25 lineto +0.000 0.000 0.000 edgecolor +newpath 808 70 moveto +818 72 lineto +808 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Reduction gsave 10 dict begin -619 47 39 18 ellipse_path +1009 72 46 18 ellipse_path stroke gsave 10 dict begin -619 48 moveto (Reduction) 57 14.00 -0.50 alignedtext +1009 67 moveto 71 -0.5 (Reduction) alignedtext end grestore end grestore % Type_errors -> Reduction -newpath 539 32 moveto -550 34 562 36 573 38 curveto +newpath 926 72 moveto +935 72 943 72 952 72 curveto stroke -newpath 574 36 moveto -583 40 lineto -573 40 lineto +0.000 0.000 0.000 edgecolor +newpath 952 70 moveto +962 72 lineto +952 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Conv_oracle gsave 10 dict begin -740 47 46 18 ellipse_path +1147 74 55 18 ellipse_path stroke gsave 10 dict begin -740 48 moveto (Conv_oracle) 71 14.00 -0.50 alignedtext +1147 69 moveto 88 -0.5 (Conv_oracle) alignedtext end grestore end grestore % Reduction -> Conv_oracle -newpath 658 47 moveto -667 47 675 47 684 47 curveto +newpath 1056 73 moveto +1065 73 1073 73 1082 73 curveto stroke -newpath 684 45 moveto -694 47 lineto -684 50 lineto +0.000 0.000 0.000 edgecolor +newpath 1082 71 moveto +1092 73 lineto +1082 76 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Term +% Term_typing gsave 10 dict begin -1269 47 27 18 ellipse_path +355 95 57 18 ellipse_path stroke gsave 10 dict begin -1269 48 moveto (Term) 30 14.00 -0.50 alignedtext +355 90 moveto 92 -0.5 (Term_typing) alignedtext end grestore end grestore -% Term -> Univ -newpath 1294 54 moveto -1304 57 1316 61 1327 64 curveto +% Cooking +gsave 10 dict begin +489 95 40 18 ellipse_path stroke -newpath 1327 61 moveto -1336 67 lineto -1326 66 lineto +gsave 10 dict begin +489 90 moveto 58 -0.5 (Cooking) alignedtext +end grestore +end grestore + +% Term_typing -> Cooking +newpath 412 95 moveto +421 95 430 95 439 95 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 439 93 moveto +449 95 lineto +439 98 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Esubst +% Indtypes gsave 10 dict begin -1361 20 29 18 ellipse_path +489 149 40 18 ellipse_path stroke gsave 10 dict begin -1361 21 moveto (Esubst) 37 14.00 -0.50 alignedtext +489 144 moveto 59 -0.5 (Indtypes) alignedtext end grestore end grestore -% Term -> Esubst -newpath 1294 40 moveto -1304 37 1315 34 1326 31 curveto +% Term_typing -> Indtypes +newpath 390 109 moveto +409 117 432 126 451 134 curveto stroke -newpath 1325 29 moveto -1335 28 lineto -1326 34 lineto +0.000 0.000 0.000 edgecolor +newpath 451 131 moveto +459 137 lineto +449 136 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Sign +% Cooking -> Reduction +newpath 511 80 moveto +532 66 560 47 566 45 curveto +720 0 768 20 926 45 curveto +935 47 951 52 968 58 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 966 55 moveto +975 60 lineto +965 60 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Indtypes -> Typeops +newpath 530 149 moveto +541 149 552 149 563 149 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 563 147 moveto +573 149 lineto +563 152 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Term gsave 10 dict begin -1179 47 27 18 ellipse_path +1726 145 30 18 ellipse_path stroke gsave 10 dict begin -1179 48 moveto (Sign) 25 14.00 -0.50 alignedtext +1726 140 moveto 38 -0.5 (Term) alignedtext end grestore end grestore -% Sign -> Term -newpath 1206 47 moveto -1214 47 1223 47 1232 47 curveto +% Term -> Univ +newpath 1754 152 moveto +1765 155 1779 159 1791 162 curveto stroke -newpath 1232 45 moveto -1242 47 lineto -1232 50 lineto +0.000 0.000 0.000 edgecolor +newpath 1791 159 moveto +1800 165 lineto +1790 164 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Safe_typing +% Esubst gsave 10 dict begin -52 46 44 18 ellipse_path +1826 118 33 18 ellipse_path stroke gsave 10 dict begin -52 47 moveto (Safe_typing) 67 14.00 -0.50 alignedtext +1826 113 moveto 45 -0.5 (Esubst) alignedtext end grestore end grestore -% Cooking +% Term -> Esubst +newpath 1754 138 moveto +1764 135 1776 132 1787 129 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1786 127 moveto +1796 126 lineto +1787 132 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Subtyping gsave 10 dict begin -273 72 34 18 ellipse_path +613 72 46 18 ellipse_path stroke gsave 10 dict begin -273 73 moveto (Cooking) 48 14.00 -0.50 alignedtext +613 67 moveto 71 -0.5 (Subtyping) alignedtext end grestore end grestore -% Safe_typing -> Cooking -newpath 94 51 moveto -134 56 192 63 231 67 curveto +% Subtyping -> Inductive +newpath 660 72 moveto +669 72 677 72 686 72 curveto stroke -newpath 229 64 moveto -239 68 lineto -229 69 lineto +0.000 0.000 0.000 edgecolor +newpath 686 70 moveto +696 72 lineto +686 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Indtypes +% Modops gsave 10 dict begin -167 22 34 18 ellipse_path +739 126 38 18 ellipse_path stroke gsave 10 dict begin -167 23 moveto (Indtypes) 48 14.00 -0.50 alignedtext +739 121 moveto 55 -0.5 (Modops) alignedtext end grestore end grestore -% Safe_typing -> Indtypes -newpath 91 38 moveto -102 36 114 33 125 31 curveto +% Subtyping -> Modops +newpath 644 85 moveto +662 93 684 102 702 110 curveto stroke -newpath 125 29 moveto -135 29 lineto -126 33 lineto +0.000 0.000 0.000 edgecolor +newpath 703 108 moveto +711 114 lineto +701 112 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Cooking -> Reduction -newpath 307 70 moveto -369 65 500 56 571 51 curveto +% Modops -> Entries +newpath 771 136 moveto +790 142 814 150 833 156 curveto stroke -newpath 570 49 moveto -580 50 lineto -570 54 lineto +0.000 0.000 0.000 edgecolor +newpath 833 153 moveto +842 159 lineto +832 158 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Indtypes -> Typeops -newpath 201 21 moveto -211 21 221 20 232 20 curveto +% Environ +gsave 10 dict begin +1387 122 39 18 ellipse_path stroke -newpath 229 18 moveto -239 20 lineto -229 23 lineto +gsave 10 dict begin +1387 117 moveto 56 -0.5 (Environ) alignedtext +end grestore +end grestore + +% Modops -> Environ +newpath 777 125 moveto +830 124 926 122 1009 122 curveto +1009 122 1009 122 1147 122 curveto +1152 122 1270 122 1339 122 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1338 120 moveto +1348 122 lineto +1338 125 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Closure +% Sign -> Term +newpath 1660 145 moveto +1668 145 1677 145 1686 145 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1686 143 moveto +1696 145 lineto +1686 148 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Safe_typing gsave 10 dict begin -854 47 32 18 ellipse_path +62 72 53 18 ellipse_path stroke gsave 10 dict begin -854 48 moveto (Closure) 43 14.00 -0.50 alignedtext +62 67 moveto 85 -0.5 (Safe_typing) alignedtext end grestore end grestore -% Conv_oracle -> Closure -newpath 786 47 moveto -795 47 804 47 812 47 curveto +% Mod_typing +gsave 10 dict begin +207 72 54 18 ellipse_path +stroke +gsave 10 dict begin +207 67 moveto 87 -0.5 (Mod_typing) alignedtext +end grestore +end grestore + +% Safe_typing -> Mod_typing +newpath 116 72 moveto +125 72 133 72 142 72 curveto stroke -newpath 812 45 moveto -822 47 lineto -812 50 lineto +0.000 0.000 0.000 edgecolor +newpath 142 70 moveto +152 72 lineto +142 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Environ +% Mod_typing -> Term_typing +newpath 257 80 moveto +269 82 282 84 294 86 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 294 84 moveto +304 87 lineto +294 88 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Mod_typing -> Subtyping +newpath 261 69 moveto +273 69 286 68 298 68 curveto +402 66 427 66 530 68 curveto +536 68 547 69 559 69 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 557 66 moveto +567 70 lineto +557 71 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Closure gsave 10 dict begin -955 47 33 18 ellipse_path +1275 75 37 18 ellipse_path stroke gsave 10 dict begin -955 48 moveto (Environ) 45 14.00 -0.50 alignedtext +1275 70 moveto 52 -0.5 (Closure) alignedtext end grestore end grestore +% Conv_oracle -> Closure +newpath 1202 74 moveto +1211 74 1220 75 1228 75 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1228 73 moveto +1238 75 lineto +1228 78 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + % Declarations gsave 10 dict begin -1070 47 45 18 ellipse_path +1516 122 53 18 ellipse_path stroke gsave 10 dict begin -1070 48 moveto (Declarations) 70 14.00 -0.50 alignedtext +1516 117 moveto 85 -0.5 (Declarations) alignedtext end grestore end grestore % Environ -> Declarations -newpath 988 47 moveto -996 47 1005 47 1014 47 curveto +newpath 1426 122 moveto +1434 122 1443 122 1452 122 curveto stroke -newpath 1014 45 moveto -1024 47 lineto -1014 50 lineto +0.000 0.000 0.000 edgecolor +newpath 1452 120 moveto +1462 122 lineto +1452 125 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Declarations -> Sign -newpath 1116 47 moveto -1125 47 1134 47 1142 47 curveto +newpath 1562 131 moveto +1574 133 1587 136 1598 138 curveto stroke -newpath 1142 45 moveto -1152 47 lineto -1142 50 lineto +0.000 0.000 0.000 edgecolor +newpath 1598 135 moveto +1607 140 lineto +1597 140 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Closure -> Environ -newpath 886 47 moveto -894 47 903 47 912 47 curveto +newpath 1303 87 moveto +1317 93 1334 100 1349 106 curveto stroke -newpath 912 45 moveto -922 47 lineto -912 50 lineto +0.000 0.000 0.000 edgecolor +newpath 1350 104 moveto +1358 110 lineto +1348 108 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/doc/library.dep.ps b/doc/library.dep.ps index fc4b9f01e..7ce732adb 100644 --- a/doc/library.dep.ps +++ b/doc/library.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (jacek) Jacek Chrzaszcz +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 142 +%%BoundingBox: 35 35 577 174 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,298 +225,377 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 142 +%%PageBoundingBox: 36 36 577 174 %%PageOrientation: Portrait gsave -35 35 541 107 boxprim clip newpath +35 35 542 139 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7317 set_scale +0.5444 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 576 142] /PAGES pdfmark +[ /CropBox [36 36 577 174] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Summary gsave 10 dict begin -580 126 37 18 ellipse_path +688 134 45 18 ellipse_path stroke gsave 10 dict begin -580 127 moveto (Summary) 54 14.00 -0.50 alignedtext +688 129 moveto 69 -0.5 (Summary) alignedtext end grestore end grestore % Libnames gsave 10 dict begin -692 76 38 18 ellipse_path +815 107 44 18 ellipse_path stroke gsave 10 dict begin -692 77 moveto (Libnames) 55 14.00 -0.50 alignedtext +815 102 moveto 67 -0.5 (Libnames) alignedtext end grestore end grestore % Summary -> Libnames -newpath 608 114 moveto -622 107 640 99 655 92 curveto +newpath 728 125 moveto +740 123 753 120 765 117 curveto stroke -newpath 654 90 moveto -664 88 lineto -656 94 lineto +0.000 0.000 0.000 edgecolor +newpath 765 115 moveto +775 115 lineto +766 119 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Nameops +gsave 10 dict begin +940 107 43 18 ellipse_path +stroke +gsave 10 dict begin +940 102 moveto 65 -0.5 (Nameops) alignedtext +end grestore +end grestore + +% Libnames -> Nameops +newpath 860 107 moveto +869 107 877 107 886 107 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 886 105 moveto +896 107 lineto +886 110 lineto +closepath +fill +0.000 0.000 0.000 edgecolor % States gsave 10 dict begin -40 72 27 18 ellipse_path +38 234 30 18 ellipse_path stroke gsave 10 dict begin -40 73 moveto (States) 33 14.00 -0.50 alignedtext +38 229 moveto 38 -0.5 (States) alignedtext end grestore end grestore % Library gsave 10 dict begin -139 72 31 18 ellipse_path +142 234 37 18 ellipse_path stroke gsave 10 dict begin -139 73 moveto (Library) 41 14.00 -0.50 alignedtext +142 229 moveto 53 -0.5 (Library) alignedtext end grestore end grestore % States -> Library -newpath 67 72 moveto -77 72 88 72 98 72 curveto +newpath 68 234 moveto +76 234 85 234 94 234 curveto stroke -newpath 98 70 moveto -108 72 lineto -98 75 lineto +0.000 0.000 0.000 edgecolor +newpath 94 232 moveto +104 234 lineto +94 237 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Declaremods gsave 10 dict begin -253 72 47 18 ellipse_path +298 234 55 18 ellipse_path stroke gsave 10 dict begin -253 73 moveto (Declaremods) 73 14.00 -0.50 alignedtext +298 229 moveto 89 -0.5 (Declaremods) alignedtext end grestore end grestore % Library -> Declaremods -newpath 170 72 moveto -178 72 187 72 196 72 curveto +newpath 180 234 moveto +196 234 215 234 232 234 curveto stroke -newpath 196 70 moveto -206 72 lineto -196 75 lineto +0.000 0.000 0.000 edgecolor +newpath 232 232 moveto +242 234 lineto +232 237 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Nametab gsave 10 dict begin -469 80 35 18 ellipse_path +563 126 43 18 ellipse_path stroke gsave 10 dict begin -469 81 moveto (Nametab) 50 14.00 -0.50 alignedtext +563 121 moveto 64 -0.5 (Nametab) alignedtext end grestore end grestore % Nametab -> Summary -newpath 497 91 moveto -511 97 528 104 543 110 curveto +newpath 606 129 moveto +615 130 624 130 633 130 curveto stroke -newpath 544 108 moveto -552 114 lineto -542 112 lineto +0.000 0.000 0.000 edgecolor +newpath 633 128 moveto +643 131 lineto +633 132 lineto closepath -gsave 0 setgray stroke grestore fill - -% Nameops -gsave 10 dict begin -580 72 36 18 ellipse_path -stroke -gsave 10 dict begin -580 73 moveto (Nameops) 52 14.00 -0.50 alignedtext -end grestore -end grestore - -% Nametab -> Nameops -newpath 504 77 moveto -514 76 524 75 534 75 curveto -stroke -newpath 534 73 moveto -544 74 lineto -534 77 lineto -closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Lib gsave 10 dict begin -366 72 27 18 ellipse_path +450 99 27 18 ellipse_path stroke gsave 10 dict begin -366 73 moveto (Lib) 19 14.00 -0.50 alignedtext +450 94 moveto 23 -0.5 (Lib) alignedtext end grestore end grestore % Declaremods -> Lib -newpath 300 72 moveto -310 72 320 72 329 72 curveto +newpath 346 225 moveto +358 221 370 215 380 207 curveto +405 186 399 171 416 145 curveto +421 138 427 130 432 123 curveto stroke -newpath 329 70 moveto -339 72 lineto -329 75 lineto +0.000 0.000 0.000 edgecolor +newpath 430 122 moveto +437 115 lineto +434 125 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Global gsave 10 dict begin -366 126 29 18 ellipse_path +450 172 33 18 ellipse_path stroke gsave 10 dict begin -366 127 moveto (Global) 38 14.00 -0.50 alignedtext +450 167 moveto 45 -0.5 (Global) alignedtext end grestore end grestore % Declaremods -> Global -newpath 282 86 moveto -298 94 318 103 334 111 curveto +newpath 337 221 moveto +358 214 379 207 380 207 curveto +393 201 406 195 418 189 curveto stroke -newpath 334 108 moveto -342 115 lineto -332 113 lineto +0.000 0.000 0.000 edgecolor +newpath 416 187 moveto +426 185 lineto +418 192 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Libobject gsave 10 dict begin -469 26 37 18 ellipse_path +688 80 43 18 ellipse_path stroke gsave 10 dict begin -469 27 moveto (Libobject) 53 14.00 -0.50 alignedtext +688 75 moveto 65 -0.5 (Libobject) alignedtext end grestore end grestore % Libobject -> Libnames -newpath 506 29 moveto -540 31 589 36 618 42 curveto -629 44 645 51 658 57 curveto +newpath 727 88 moveto +739 90 753 93 766 96 curveto stroke -newpath 659 55 moveto -667 62 lineto -657 59 lineto +0.000 0.000 0.000 edgecolor +newpath 767 94 moveto +776 98 lineto +766 98 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Lib -> Nametab -newpath 393 74 moveto -404 75 415 76 427 77 curveto +newpath 476 105 moveto +489 108 504 112 519 115 curveto stroke -newpath 424 75 moveto -434 77 lineto -424 80 lineto +0.000 0.000 0.000 edgecolor +newpath 517 112 moveto +526 117 lineto +516 117 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Lib -> Libobject -newpath 389 62 moveto -401 56 418 49 432 42 curveto +newpath 477 97 moveto +516 94 589 88 638 84 curveto stroke -newpath 431 40 moveto -441 38 lineto -433 44 lineto +0.000 0.000 0.000 edgecolor +newpath 635 82 moveto +645 83 lineto +635 87 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Impargs gsave 10 dict begin -253 126 33 18 ellipse_path +298 126 39 18 ellipse_path stroke gsave 10 dict begin -253 127 moveto (Impargs) 45 14.00 -0.50 alignedtext +298 121 moveto 56 -0.5 (Impargs) alignedtext end grestore end grestore % Impargs -> Lib -newpath 278 114 moveto -295 106 318 95 336 86 curveto +newpath 334 120 moveto +359 116 391 110 415 105 curveto stroke -newpath 334 84 moveto -344 82 lineto -336 89 lineto +0.000 0.000 0.000 edgecolor +newpath 414 103 moveto +424 104 lineto +414 108 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Impargs -> Global -newpath 286 126 moveto -299 126 314 126 327 126 curveto +newpath 331 136 moveto +355 143 387 153 412 161 curveto stroke -newpath 326 124 moveto -336 126 lineto -326 129 lineto +0.000 0.000 0.000 edgecolor +newpath 412 158 moveto +421 163 lineto +411 163 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Global -> Summary -newpath 396 126 moveto -431 126 492 126 533 126 curveto +newpath 483 169 moveto +515 166 564 160 606 153 curveto +617 151 629 148 640 146 curveto stroke -newpath 532 124 moveto -542 126 lineto -532 129 lineto +0.000 0.000 0.000 edgecolor +newpath 639 144 moveto +649 144 lineto +640 149 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Goptions gsave 10 dict begin -253 18 36 18 ellipse_path +298 72 42 18 ellipse_path stroke gsave 10 dict begin -253 19 moveto (Goptions) 51 14.00 -0.50 alignedtext +298 67 moveto 62 -0.5 (Goptions) alignedtext end grestore end grestore % Goptions -> Lib -newpath 279 31 moveto -296 39 318 49 336 57 curveto +newpath 337 79 moveto +361 83 392 89 415 93 curveto stroke -newpath 336 54 moveto -344 61 lineto -334 59 lineto +0.000 0.000 0.000 edgecolor +newpath 414 90 moveto +424 94 lineto +414 95 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Declare +% Dischargedhypsmap gsave 10 dict begin -40 126 32 18 ellipse_path +298 18 81 18 ellipse_path stroke gsave 10 dict begin -40 127 moveto (Declare) 43 14.00 -0.50 alignedtext +298 13 moveto 141 -0.5 (Dischargedhypsmap) alignedtext end grestore end grestore -% Declare -> Library -newpath 63 113 moveto -76 105 93 97 108 89 curveto +% Dischargedhypsmap -> Lib +newpath 344 33 moveto +363 39 380 45 380 45 curveto +397 54 415 68 428 79 curveto stroke -newpath 106 87 moveto -116 84 lineto -109 91 lineto +0.000 0.000 0.000 edgecolor +newpath 428 76 moveto +434 84 lineto +425 80 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Declare +gsave 10 dict begin +142 126 37 18 ellipse_path +stroke +gsave 10 dict begin +142 121 moveto 52 -0.5 (Declare) alignedtext +end grestore +end grestore % Declare -> Impargs -newpath 72 126 moveto -109 126 171 126 212 126 curveto +newpath 179 126 moveto +200 126 227 126 250 126 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 249 124 moveto +259 126 lineto +249 129 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Declare -> Dischargedhypsmap +newpath 157 109 moveto +178 86 213 48 216 45 curveto +221 42 230 38 241 35 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 239 33 moveto +249 32 lineto +241 38 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Decl_kinds +gsave 10 dict begin +298 180 50 18 ellipse_path +stroke +gsave 10 dict begin +298 175 moveto 78 -0.5 (Decl_kinds) alignedtext +end grestore +end grestore + +% Declare -> Decl_kinds +newpath 172 137 moveto +189 143 208 150 216 153 curveto +228 157 240 161 252 165 curveto stroke -newpath 210 124 moveto -220 126 lineto -210 129 lineto +0.000 0.000 0.000 edgecolor +newpath 252 162 moveto +261 168 lineto +251 167 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps index 9df862840..be76f7404 100644 --- a/doc/parsing.dep.ps +++ b/doc/parsing.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (herbelin) Hugo Herbelin +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 232 +%%BoundingBox: 35 35 577 196 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,384 +225,481 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 232 +%%PageBoundingBox: 36 36 577 196 %%PageOrientation: Portrait gsave -35 35 541 197 boxprim clip newpath +35 35 542 161 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7584 set_scale +0.6767 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 576 232] /PAGES pdfmark +[ /CropBox [36 36 577 196] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Pcoq gsave 10 dict begin -581 103 27 18 ellipse_path +441 180 27 18 ellipse_path stroke gsave 10 dict begin -581 104 moveto (Pcoq) 28 14.00 -0.50 alignedtext +441 175 moveto 33 -0.5 (Pcoq) alignedtext end grestore end grestore -% Coqast +% Extend gsave 10 dict begin -674 103 30 18 ellipse_path +552 126 35 18 ellipse_path stroke gsave 10 dict begin -674 104 moveto (Coqast) 38 14.00 -0.50 alignedtext +552 121 moveto 49 -0.5 (Extend) alignedtext end grestore end grestore -% Pcoq -> Coqast -newpath 608 103 moveto -616 103 625 103 634 103 curveto +% Pcoq -> Extend +newpath 463 169 moveto +478 161 500 151 517 143 curveto stroke -newpath 634 101 moveto -644 103 lineto -634 106 lineto +0.000 0.000 0.000 edgecolor +newpath 516 141 moveto +526 139 lineto +518 145 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Extend +% Ast gsave 10 dict begin -398 52 30 18 ellipse_path +655 72 27 18 ellipse_path stroke gsave 10 dict begin -398 53 moveto (Extend) 39 14.00 -0.50 alignedtext +655 67 moveto 23 -0.5 (Ast) alignedtext end grestore end grestore -% Ast +% Extend -> Ast +newpath 577 113 moveto +591 105 610 96 626 87 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 624 85 moveto +634 83 lineto +626 90 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Lexer gsave 10 dict begin -491 103 27 18 ellipse_path +655 126 31 18 ellipse_path stroke gsave 10 dict begin -491 104 moveto (Ast) 19 14.00 -0.50 alignedtext +655 121 moveto 40 -0.5 (Lexer) alignedtext end grestore end grestore -% Extend -> Ast -newpath 421 64 moveto -433 71 448 79 462 86 curveto +% Extend -> Lexer +newpath 588 126 moveto +597 126 606 126 614 126 curveto stroke -newpath 463 84 moveto -470 91 lineto -460 88 lineto +0.000 0.000 0.000 edgecolor +newpath 614 124 moveto +624 126 lineto +614 129 lineto closepath -gsave 0 setgray stroke grestore fill - -% Ast -> Pcoq -newpath 518 103 moveto -526 103 535 103 544 103 curveto -stroke -newpath 544 101 moveto -554 103 lineto -544 106 lineto -closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Termast gsave 10 dict begin -292 156 33 18 ellipse_path +441 72 39 18 ellipse_path stroke gsave 10 dict begin -292 157 moveto (Termast) 45 14.00 -0.50 alignedtext +441 67 moveto 56 -0.5 (Termast) alignedtext end grestore end grestore % Termast -> Ast -newpath 325 152 moveto -355 149 401 143 428 136 curveto -438 133 451 127 462 120 curveto +newpath 480 72 moveto +520 72 581 72 620 72 curveto stroke -newpath 461 118 moveto -471 115 lineto -463 122 lineto +0.000 0.000 0.000 edgecolor +newpath 618 70 moveto +628 72 lineto +618 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Search +% Coqast gsave 10 dict begin -48 198 29 18 ellipse_path +756 72 34 18 ellipse_path stroke gsave 10 dict begin -48 199 moveto (Search) 37 14.00 -0.50 alignedtext +756 67 moveto 46 -0.5 (Coqast) alignedtext end grestore end grestore -% Astterm +% Ast -> Coqast +newpath 682 72 moveto +691 72 702 72 712 72 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 712 70 moveto +722 72 lineto +712 75 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Search gsave 10 dict begin -170 94 33 18 ellipse_path +46 122 33 18 ellipse_path stroke gsave 10 dict begin -170 95 moveto (Astterm) 45 14.00 -0.50 alignedtext +46 117 moveto 45 -0.5 (Search) alignedtext end grestore end grestore -% Search -> Astterm -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 +% Printer gsave 10 dict begin -292 229 29 18 ellipse_path +169 122 34 18 ellipse_path stroke gsave 10 dict begin -292 230 moveto (Coqlib) 38 14.00 -0.50 alignedtext +169 117 moveto 47 -0.5 (Printer) alignedtext end grestore end grestore -% Search -> Coqlib -newpath 70 210 moveto -87 218 109 229 124 232 curveto -159 239 217 235 255 233 curveto +% Search -> Printer +newpath 80 122 moveto +94 122 110 122 124 122 curveto stroke -newpath 253 231 moveto -263 232 lineto -253 236 lineto +0.000 0.000 0.000 edgecolor +newpath 124 120 moveto +134 122 lineto +124 125 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Printer +% Ppconstr gsave 10 dict begin -170 148 29 18 ellipse_path +310 72 40 18 ellipse_path stroke gsave 10 dict begin -170 149 moveto (Printer) 38 14.00 -0.50 alignedtext +310 67 moveto 59 -0.5 (Ppconstr) alignedtext end grestore end grestore -% Search -> Printer -newpath 73 188 moveto -91 180 116 170 137 162 curveto +% Printer -> Ppconstr +newpath 198 112 moveto +218 105 246 95 269 86 curveto stroke -newpath 135 160 moveto -145 158 lineto -137 165 lineto +0.000 0.000 0.000 edgecolor +newpath 268 84 moveto +278 83 lineto +269 89 lineto closepath -gsave 0 setgray stroke grestore fill - -% Astterm -> Termast -newpath 194 106 moveto -213 116 239 129 260 139 curveto -stroke -newpath 260 136 moveto -268 143 lineto -258 141 lineto +fill +0.000 0.000 0.000 edgecolor + +% Ppconstr -> Pcoq +newpath 340 84 moveto +351 89 362 95 366 99 curveto +388 117 382 132 402 153 curveto +406 157 409 160 413 163 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 414 161 moveto +421 168 lineto +411 165 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Printer -> Termast -newpath 200 150 moveto -215 151 233 152 249 153 curveto +% Ppconstr -> Termast +newpath 351 72 moveto +364 72 379 72 392 72 curveto stroke -newpath 249 151 moveto -259 154 lineto -249 155 lineto +0.000 0.000 0.000 edgecolor +newpath 392 70 moveto +402 72 lineto +392 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Esyntax gsave 10 dict begin -292 48 33 18 ellipse_path +441 126 39 18 ellipse_path stroke gsave 10 dict begin -292 49 moveto (Esyntax) 45 14.00 -0.50 alignedtext +441 121 moveto 56 -0.5 (Esyntax) alignedtext end grestore end grestore -% Printer -> Esyntax -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 +% Ppconstr -> Esyntax +newpath 340 84 moveto +358 92 383 102 403 110 curveto stroke -newpath 258 64 moveto -268 61 lineto -260 68 lineto +0.000 0.000 0.000 edgecolor +newpath 404 108 moveto +412 114 lineto +402 112 lineto closepath -gsave 0 setgray stroke grestore fill - -% Esyntax -> Extend -newpath 325 49 moveto -336 49 348 50 359 50 curveto -stroke -newpath 358 47 moveto -368 51 lineto -358 52 lineto -closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Prettyp gsave 10 dict begin -48 144 30 18 ellipse_path +46 68 36 18 ellipse_path stroke gsave 10 dict begin -48 145 moveto (Prettyp) 40 14.00 -0.50 alignedtext +46 63 moveto 50 -0.5 (Prettyp) alignedtext end grestore end grestore % Prettyp -> Printer -newpath 78 145 moveto -94 146 114 146 131 147 curveto +newpath 73 80 moveto +91 88 115 98 134 106 curveto stroke -newpath 130 145 moveto -140 147 lineto -130 150 lineto +0.000 0.000 0.000 edgecolor +newpath 134 103 moveto +142 110 lineto +132 108 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% G_zsyntax +% Printmod gsave 10 dict begin -48 86 40 18 ellipse_path +169 68 43 18 ellipse_path stroke gsave 10 dict begin -48 87 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext +169 63 moveto 65 -0.5 (Printmod) alignedtext end grestore end grestore -% G_zsyntax -> Astterm -newpath 88 89 moveto -101 90 115 91 128 91 curveto +% Prettyp -> Printmod +newpath 82 68 moveto +93 68 104 68 115 68 curveto stroke -newpath 127 88 moveto -137 92 lineto -127 93 lineto +0.000 0.000 0.000 edgecolor +newpath 115 66 moveto +125 68 lineto +115 71 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% G_zsyntax -> Esyntax -newpath 80 75 moveto -95 71 112 66 124 64 curveto -159 58 214 54 251 51 curveto +% Pptactic +gsave 10 dict begin +46 188 38 18 ellipse_path stroke -newpath 249 49 moveto -259 50 lineto -249 54 lineto +gsave 10 dict begin +46 183 moveto 54 -0.5 (Pptactic) alignedtext +end grestore +end grestore + +% Pptactic -> Printer +newpath 71 174 moveto +90 164 116 150 137 139 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 135 137 moveto +145 135 lineto +137 142 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% G_rsyntax +% Egrammar gsave 10 dict begin -48 25 39 18 ellipse_path +169 213 48 18 ellipse_path stroke gsave 10 dict begin -48 26 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext +169 208 moveto 75 -0.5 (Egrammar) alignedtext end grestore end grestore -% G_rsyntax -> Astterm -newpath 73 39 moveto -92 50 119 65 139 77 curveto +% Pptactic -> Egrammar +newpath 81 195 moveto +92 197 104 200 116 202 curveto stroke -newpath 139 74 moveto -147 81 lineto -137 79 lineto +0.000 0.000 0.000 edgecolor +newpath 117 200 moveto +126 204 lineto +116 204 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Egrammar -> Pcoq +newpath 217 216 moveto +257 217 316 216 366 207 curveto +374 205 392 199 407 193 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 407 190 moveto +417 189 lineto +409 195 lineto +closepath +fill +0.000 0.000 0.000 edgecolor -% G_rsyntax -> Esyntax -newpath 88 26 moveto -126 26 182 28 216 31 curveto -226 32 242 35 255 38 curveto +% Esyntax -> Extend +newpath 480 126 moveto +489 126 498 126 506 126 curveto stroke -newpath 253 35 moveto -262 40 lineto -252 40 lineto +0.000 0.000 0.000 edgecolor +newpath 506 124 moveto +516 126 lineto +506 129 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% G_natsyntax +% G_zsyntax gsave 10 dict begin -170 202 45 18 ellipse_path +310 18 49 18 ellipse_path stroke gsave 10 dict begin -170 203 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext +310 13 moveto 76 -0.5 (G_zsyntax) alignedtext end grestore end grestore -% G_natsyntax -> Termast -newpath 203 190 moveto -219 184 239 176 256 169 curveto +% G_zsyntax -> Pcoq +newpath 346 30 moveto +353 34 361 39 366 45 curveto +400 82 372 112 402 153 curveto +405 156 408 160 412 162 curveto stroke -newpath 255 167 moveto -265 166 lineto -256 172 lineto +0.000 0.000 0.000 edgecolor +newpath 413 160 moveto +420 168 lineto +411 164 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% G_natsyntax -> Coqlib -newpath 210 211 moveto -225 214 241 218 255 221 curveto +% G_zsyntax -> Termast +newpath 343 31 moveto +361 39 385 48 404 56 curveto stroke -newpath 255 218 moveto -264 223 lineto -254 223 lineto +0.000 0.000 0.000 edgecolor +newpath 404 53 moveto +412 60 lineto +402 58 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% G_natsyntax -> Esyntax -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 +% G_zsyntax -> Esyntax +newpath 342 32 moveto +352 36 362 41 366 45 curveto +388 64 382 78 402 99 curveto +404 101 407 104 409 106 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 410 104 moveto +417 112 lineto +408 108 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Egrammar +% G_rsyntax gsave 10 dict begin -292 102 40 18 ellipse_path +310 180 48 18 ellipse_path stroke gsave 10 dict begin -292 103 moveto (Egrammar) 58 14.00 -0.50 alignedtext +310 175 moveto 74 -0.5 (G_rsyntax) alignedtext end grestore end grestore -% Egrammar -> Extend -newpath 320 89 moveto -334 82 351 74 366 67 curveto +% G_rsyntax -> Pcoq +newpath 358 180 moveto +373 180 389 180 404 180 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 403 178 moveto +413 180 lineto +403 183 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% G_rsyntax -> Termast +newpath 342 166 moveto +352 162 362 157 366 153 curveto +388 134 382 119 402 99 curveto +404 96 407 94 409 92 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 407 90 moveto +417 86 lineto +411 94 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% G_rsyntax -> Esyntax +newpath 342 167 moveto +360 159 384 150 403 142 curveto stroke -newpath 364 65 moveto -374 63 lineto -366 70 lineto +0.000 0.000 0.000 edgecolor +newpath 402 140 moveto +412 138 lineto +404 144 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Lexer +% G_natsyntax gsave 10 dict begin -398 106 27 18 ellipse_path +310 126 56 18 ellipse_path stroke gsave 10 dict begin -398 107 moveto (Lexer) 32 14.00 -0.50 alignedtext +310 121 moveto 90 -0.5 (G_natsyntax) alignedtext end grestore end grestore -% Egrammar -> Lexer -newpath 332 104 moveto -342 104 352 105 361 105 curveto +% G_natsyntax -> Pcoq +newpath 345 140 moveto +365 149 391 159 410 167 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 410 164 moveto +418 170 lineto +408 169 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% G_natsyntax -> Termast +newpath 345 112 moveto +363 104 385 95 403 87 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 402 85 moveto +412 84 lineto +403 90 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% G_natsyntax -> Esyntax +newpath 366 126 moveto +375 126 384 126 392 126 curveto stroke -newpath 361 103 moveto -371 105 lineto -361 108 lineto +0.000 0.000 0.000 edgecolor +newpath 392 124 moveto +402 126 lineto +392 129 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps index e6a242ac4..ffa9c5302 100644 --- a/doc/pretyping.dep.ps +++ b/doc/pretyping.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (herbelin) Hugo Herbelin +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 577 201 +%%BoundingBox: 35 35 577 159 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,533 +225,538 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 577 201 +%%PageBoundingBox: 36 36 577 159 %%PageOrientation: Portrait gsave -35 35 542 166 boxprim clip newpath +35 35 542 124 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.4796 set_scale +0.3634 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 577 201] /PAGES pdfmark +[ /CropBox [36 36 577 159] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font -% Multcase -gsave 10 dict begin -355 272 36 18 ellipse_path -stroke -gsave 10 dict begin -355 273 moveto (Multcase) 51 14.00 -0.50 alignedtext -end grestore -end grestore - -% Evarutil +% Typing gsave 10 dict begin -468 272 33 18 ellipse_path +523 241 36 18 ellipse_path stroke gsave 10 dict begin -468 273 moveto (Evarutil) 45 14.00 -0.50 alignedtext +523 236 moveto 50 -0.5 (Typing) alignedtext end grestore end grestore -% Multcase -> Evarutil -newpath 391 272 moveto -402 272 414 272 425 272 curveto -stroke -newpath 425 270 moveto -435 272 lineto -425 275 lineto -closepath -gsave 0 setgray stroke grestore fill - % Pretype_errors gsave 10 dict begin -596 272 51 18 ellipse_path +898 264 62 18 ellipse_path stroke gsave 10 dict begin -596 273 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext -end grestore -end grestore - -% Evarutil -> Pretype_errors -newpath 501 272 moveto -511 272 523 272 534 272 curveto -stroke -newpath 534 270 moveto -544 272 lineto -534 275 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Indrec -gsave 10 dict begin -596 326 28 18 ellipse_path -stroke -gsave 10 dict begin -596 327 moveto (Indrec) 35 14.00 -0.50 alignedtext -end grestore -end grestore - -% Evarutil -> Indrec -newpath 494 283 moveto -514 292 542 304 564 313 curveto -stroke -newpath 564 310 moveto -572 316 lineto -562 315 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Typing -gsave 10 dict begin -468 218 30 18 ellipse_path -stroke -gsave 10 dict begin -468 219 moveto (Typing) 40 14.00 -0.50 alignedtext +898 259 moveto 102 -0.5 (Pretype_errors) alignedtext end grestore end grestore % Typing -> Pretype_errors -newpath 493 229 moveto -510 236 534 246 554 254 curveto +newpath 559 243 moveto +621 247 750 255 830 260 curveto stroke -newpath 555 252 moveto -563 258 lineto -553 256 lineto +0.000 0.000 0.000 edgecolor +newpath 827 258 moveto +837 260 lineto +827 263 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Rawterm gsave 10 dict begin -731 164 36 18 ellipse_path +1051 114 43 18 ellipse_path stroke gsave 10 dict begin -731 165 moveto (Rawterm) 51 14.00 -0.50 alignedtext +1051 109 moveto 65 -0.5 (Rawterm) alignedtext end grestore end grestore % Pretype_errors -> Rawterm -newpath 630 258 moveto -637 255 644 251 648 248 curveto -667 233 692 206 710 187 curveto -stroke -newpath 708 186 moveto -716 180 lineto -711 189 lineto +newpath 939 250 moveto +946 247 954 242 960 237 curveto +983 218 979 206 996 183 curveto +1008 168 1021 151 1032 138 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1029 138 moveto +1037 131 lineto +1033 141 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Inductiveops gsave 10 dict begin -731 245 46 18 ellipse_path +1051 210 54 18 ellipse_path stroke gsave 10 dict begin -731 246 moveto (Inductiveops) 72 14.00 -0.50 alignedtext +1051 205 moveto 87 -0.5 (Inductiveops) alignedtext end grestore end grestore % Pretype_errors -> Inductiveops -newpath 641 263 moveto -654 261 667 258 680 255 curveto +newpath 937 250 moveto +958 243 984 234 1005 226 curveto stroke -newpath 679 253 moveto -689 253 lineto -680 258 lineto +0.000 0.000 0.000 edgecolor +newpath 1004 224 moveto +1014 223 lineto +1005 229 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Tacred gsave 10 dict begin -731 56 29 18 ellipse_path +761 120 34 18 ellipse_path stroke gsave 10 dict begin -731 57 moveto (Tacred) 38 14.00 -0.50 alignedtext +761 115 moveto 47 -0.5 (Tacred) alignedtext end grestore end grestore % Cbv gsave 10 dict begin -863 56 27 18 ellipse_path +1200 18 27 18 ellipse_path stroke gsave 10 dict begin -863 57 moveto (Cbv) 23 14.00 -0.50 alignedtext +1200 13 moveto 29 -0.5 (Cbv) alignedtext end grestore end grestore % Tacred -> Cbv -newpath 761 56 moveto -781 56 806 56 827 56 curveto +newpath 775 103 moveto +794 80 828 41 836 37 curveto +852 30 1077 22 1165 19 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1163 17 moveto +1173 19 lineto +1163 22 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Tacred -> Rawterm +newpath 796 119 moveto +847 118 941 116 999 115 curveto stroke -newpath 826 54 moveto -836 56 lineto -826 59 lineto +0.000 0.000 0.000 edgecolor +newpath 997 113 moveto +1007 115 lineto +997 118 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Reductionops +% Retyping gsave 10 dict begin -863 110 49 18 ellipse_path +898 210 43 18 ellipse_path stroke gsave 10 dict begin -863 111 moveto (Reductionops) 77 14.00 -0.50 alignedtext +898 205 moveto 64 -0.5 (Retyping) alignedtext end grestore end grestore -% Tacred -> Reductionops -newpath 756 66 moveto -774 74 800 84 821 92 curveto +% Tacred -> Retyping +newpath 779 135 moveto +801 154 835 182 836 183 curveto +837 183 847 188 859 193 curveto stroke -newpath 822 90 moveto -830 96 lineto -820 94 lineto +0.000 0.000 0.000 edgecolor +newpath 860 191 moveto +868 197 lineto +858 195 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Instantiate gsave 10 dict begin -988 56 39 18 ellipse_path +1341 18 46 18 ellipse_path stroke gsave 10 dict begin -988 57 moveto (Instantiate) 58 14.00 -0.50 alignedtext +1341 13 moveto 71 -0.5 (Instantiate) alignedtext end grestore end grestore % Cbv -> Instantiate -newpath 890 56 moveto -904 56 922 56 938 56 curveto +newpath 1227 18 moveto +1243 18 1264 18 1284 18 curveto stroke -newpath 938 54 moveto -948 56 lineto -938 59 lineto +0.000 0.000 0.000 edgecolor +newpath 1284 16 moveto +1294 18 lineto +1284 21 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Reductionops -> Instantiate -newpath 895 96 moveto -912 88 933 80 951 72 curveto +% Retyping -> Inductiveops +newpath 941 210 moveto +955 210 971 210 986 210 curveto stroke -newpath 949 70 moveto -959 68 lineto -951 75 lineto +0.000 0.000 0.000 edgecolor +newpath 986 208 moveto +996 210 lineto +986 213 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Termops +% Reductionops gsave 10 dict begin -988 110 35 18 ellipse_path +1200 72 58 18 ellipse_path stroke gsave 10 dict begin -988 111 moveto (Termops) 49 14.00 -0.50 alignedtext +1200 67 moveto 94 -0.5 (Reductionops) alignedtext end grestore end grestore -% Reductionops -> Termops -newpath 912 110 moveto -923 110 933 110 943 110 curveto +% Inductiveops -> Reductionops +newpath 1070 193 moveto +1097 169 1146 123 1175 95 curveto stroke -newpath 943 108 moveto -953 110 lineto -943 113 lineto +0.000 0.000 0.000 edgecolor +newpath 1172 94 moveto +1181 89 lineto +1176 98 lineto closepath -gsave 0 setgray stroke grestore fill - -% Syntax_def -gsave 10 dict begin -596 164 42 18 ellipse_path -stroke -gsave 10 dict begin -596 165 moveto (Syntax_def) 63 14.00 -0.50 alignedtext -end grestore -end grestore +fill +0.000 0.000 0.000 edgecolor -% Syntax_def -> Rawterm -newpath 638 164 moveto -653 164 670 164 685 164 curveto +% Reductionops -> Instantiate +newpath 1237 58 moveto +1256 51 1279 42 1299 34 curveto stroke -newpath 685 162 moveto -695 164 lineto -685 167 lineto +0.000 0.000 0.000 edgecolor +newpath 1298 32 moveto +1308 31 lineto +1299 37 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Retyping +% Termops gsave 10 dict begin -355 49 36 18 ellipse_path +1341 72 41 18 ellipse_path stroke gsave 10 dict begin -355 50 moveto (Retyping) 51 14.00 -0.50 alignedtext +1341 67 moveto 60 -0.5 (Termops) alignedtext end grestore end grestore -% Retyping -> Reductionops -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 +% Reductionops -> Termops +newpath 1258 72 moveto +1269 72 1280 72 1290 72 curveto stroke -newpath 825 90 moveto -833 96 lineto -823 94 lineto +0.000 0.000 0.000 edgecolor +newpath 1290 70 moveto +1300 72 lineto +1290 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Evd gsave 10 dict begin -1091 56 27 18 ellipse_path +1451 18 27 18 ellipse_path stroke gsave 10 dict begin -1091 57 moveto (Evd) 22 14.00 -0.50 alignedtext +1451 13 moveto 28 -0.5 (Evd) alignedtext end grestore end grestore % Instantiate -> Evd -newpath 1028 56 moveto -1037 56 1046 56 1054 56 curveto +newpath 1388 18 moveto +1397 18 1406 18 1414 18 curveto stroke -newpath 1054 54 moveto -1064 56 lineto -1054 59 lineto +0.000 0.000 0.000 edgecolor +newpath 1414 16 moveto +1424 18 lineto +1414 21 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Recordops gsave 10 dict begin -468 110 40 18 ellipse_path +523 149 47 18 ellipse_path stroke gsave 10 dict begin -468 111 moveto (Recordops) 59 14.00 -0.50 alignedtext +523 144 moveto 72 -0.5 (Recordops) alignedtext end grestore end grestore % Classops gsave 10 dict begin -596 56 35 18 ellipse_path +646 139 39 18 ellipse_path stroke gsave 10 dict begin -596 57 moveto (Classops) 49 14.00 -0.50 alignedtext +646 134 moveto 57 -0.5 (Classops) alignedtext end grestore end grestore % Recordops -> Classops -newpath 497 98 moveto -516 90 541 79 561 71 curveto +newpath 569 145 moveto +578 144 588 144 597 143 curveto stroke -newpath 559 69 moveto -569 68 lineto -561 74 lineto +0.000 0.000 0.000 edgecolor +newpath 597 141 moveto +607 142 lineto +597 145 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Classops -> Tacred -newpath 631 56 moveto -650 56 673 56 692 56 curveto -stroke -newpath 691 54 moveto -701 56 lineto -691 59 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Classops -> Rawterm -newpath 622 68 moveto -635 74 648 80 648 80 curveto -667 94 692 121 710 141 curveto +newpath 683 133 moveto +694 131 707 129 718 127 curveto stroke -newpath 711 138 moveto -716 147 lineto -707 142 lineto +0.000 0.000 0.000 edgecolor +newpath 718 125 moveto +728 125 lineto +719 129 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Pretyping gsave 10 dict begin -46 114 37 18 ellipse_path +53 241 44 18 ellipse_path stroke gsave 10 dict begin -46 115 moveto (Pretyping) 54 14.00 -0.50 alignedtext +53 236 moveto 67 -0.5 (Pretyping) alignedtext end grestore end grestore % Cases gsave 10 dict begin -147 114 27 18 ellipse_path +164 241 29 18 ellipse_path stroke gsave 10 dict begin -147 115 moveto (Cases) 32 14.00 -0.50 alignedtext +164 236 moveto 37 -0.5 (Cases) alignedtext end grestore end grestore % Pretyping -> Cases -newpath 84 114 moveto -93 114 102 114 110 114 curveto +newpath 98 241 moveto +107 241 116 241 124 241 curveto stroke -newpath 110 112 moveto -120 114 lineto -110 117 lineto +0.000 0.000 0.000 edgecolor +newpath 124 239 moveto +134 241 lineto +124 244 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Coercion gsave 10 dict begin -246 114 36 18 ellipse_path +272 241 41 18 ellipse_path stroke gsave 10 dict begin -246 115 moveto (Coercion) 51 14.00 -0.50 alignedtext +272 236 moveto 61 -0.5 (Coercion) alignedtext end grestore end grestore % Cases -> Coercion -newpath 174 114 moveto -182 114 191 114 200 114 curveto +newpath 194 241 moveto +202 241 211 241 220 241 curveto stroke -newpath 200 112 moveto -210 114 lineto -200 117 lineto +0.000 0.000 0.000 edgecolor +newpath 220 239 moveto +230 241 lineto +220 244 lineto closepath -gsave 0 setgray stroke grestore fill - -% Inductiveops -> Reductionops -newpath 748 228 moveto -771 204 815 159 841 132 curveto -stroke -newpath 837 132 moveto -846 127 lineto -841 136 lineto -closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Pattern gsave 10 dict begin -596 110 30 18 ellipse_path +898 64 35 18 ellipse_path stroke gsave 10 dict begin -596 111 moveto (Pattern) 39 14.00 -0.50 alignedtext +898 59 moveto 49 -0.5 (Pattern) alignedtext end grestore end grestore -% Pattern -> Reductionops -newpath 626 110 moveto -670 110 751 110 806 110 curveto +% Pattern -> Rawterm +newpath 928 74 moveto +950 81 982 91 1008 100 curveto stroke -newpath 804 108 moveto -814 110 lineto -804 113 lineto +0.000 0.000 0.000 edgecolor +newpath 1008 97 moveto +1017 103 lineto +1007 102 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Pattern -> Rawterm -newpath 621 120 moveto -641 129 671 140 694 150 curveto +% Pattern -> Reductionops +newpath 934 65 moveto +983 66 1072 69 1134 70 curveto stroke -newpath 694 147 moveto -703 153 lineto -693 152 lineto +0.000 0.000 0.000 edgecolor +newpath 1132 68 moveto +1142 70 lineto +1132 73 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Indrec -> Inductiveops -newpath 619 316 moveto -630 311 641 306 648 302 curveto -663 293 683 279 700 267 curveto +% Indrec +gsave 10 dict begin +898 318 32 18 ellipse_path stroke -newpath 699 265 moveto -708 261 lineto -702 269 lineto +gsave 10 dict begin +898 313 moveto 43 -0.5 (Indrec) alignedtext +end grestore +end grestore + +% Indrec -> Inductiveops +newpath 926 308 moveto +937 304 949 298 960 291 curveto +973 282 1004 255 1026 234 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1024 232 moveto +1033 227 lineto +1028 236 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Evarconv +% Evarutil gsave 10 dict begin -355 180 37 18 ellipse_path +761 287 39 18 ellipse_path stroke gsave 10 dict begin -355 181 moveto (Evarconv) 53 14.00 -0.50 alignedtext +761 282 moveto 56 -0.5 (Evarutil) alignedtext end grestore end grestore -% Evarconv -> Evarutil -newpath 372 196 moveto -388 212 412 235 428 248 curveto -431 250 433 251 436 253 curveto +% Evarutil -> Pretype_errors +newpath 798 281 moveto +809 279 822 277 834 275 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 834 273 moveto +844 273 lineto +835 277 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Evarutil -> Indrec +newpath 796 295 moveto +815 299 839 304 859 309 curveto stroke -newpath 438 251 moveto -445 259 lineto -435 256 lineto +0.000 0.000 0.000 edgecolor +newpath 859 306 moveto +868 311 lineto +858 311 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Evarconv +gsave 10 dict begin +395 241 44 18 ellipse_path +stroke +gsave 10 dict begin +395 236 moveto 67 -0.5 (Evarconv) alignedtext +end grestore +end grestore % Evarconv -> Typing -newpath 386 190 moveto -400 195 418 201 432 206 curveto +newpath 440 241 moveto +452 241 465 241 477 241 curveto stroke -newpath 432 203 moveto -441 209 lineto -431 208 lineto +0.000 0.000 0.000 edgecolor +newpath 477 239 moveto +487 241 lineto +477 244 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Evarconv -> Recordops -newpath 378 166 moveto -395 156 418 141 436 130 curveto +newpath 417 225 moveto +439 210 471 187 494 170 curveto stroke -newpath 434 128 moveto -444 125 lineto -437 132 lineto +0.000 0.000 0.000 edgecolor +newpath 491 169 moveto +501 165 lineto +494 173 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Evarconv -> Evarutil +newpath 427 254 moveto +442 259 460 264 476 268 curveto +482 269 636 278 715 284 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 712 282 moveto +722 284 lineto +712 287 lineto +closepath +fill +0.000 0.000 0.000 edgecolor % Detyping gsave 10 dict begin -596 218 36 18 ellipse_path +898 156 43 18 ellipse_path stroke gsave 10 dict begin -596 219 moveto (Detyping) 52 14.00 -0.50 alignedtext +898 151 moveto 64 -0.5 (Detyping) alignedtext end grestore end grestore % Detyping -> Rawterm -newpath 625 207 moveto -645 199 673 188 694 179 curveto +newpath 934 146 moveto +956 141 983 133 1006 127 curveto stroke -newpath 693 177 moveto -703 175 lineto -695 181 lineto +0.000 0.000 0.000 edgecolor +newpath 1005 125 moveto +1015 124 lineto +1006 130 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Detyping -> Inductiveops -newpath 630 225 moveto -645 228 663 232 679 235 curveto -stroke -newpath 680 233 moveto -689 237 lineto -679 237 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Coercion -> Retyping -newpath 269 100 moveto -285 91 306 78 323 68 curveto +newpath 931 168 moveto +952 176 981 185 1004 194 curveto stroke -newpath 321 66 moveto -331 63 lineto -324 70 lineto +0.000 0.000 0.000 edgecolor +newpath 1004 191 moveto +1013 197 lineto +1003 196 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Coercion -> Evarconv -newpath 269 128 moveto -285 138 306 151 324 161 curveto +newpath 314 241 moveto +323 241 331 241 340 241 curveto stroke -newpath 325 159 moveto -332 166 lineto -322 163 lineto +0.000 0.000 0.000 edgecolor +newpath 340 239 moveto +350 241 lineto +340 244 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps index 68b602755..bdbf33327 100644 --- a/doc/proofs.dep.ps +++ b/doc/proofs.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (herbelin) Hugo Herbelin +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 577 136 +%%BoundingBox: 35 35 577 125 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,230 +225,241 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 577 136 +%%PageBoundingBox: 36 36 577 125 %%PageOrientation: Portrait gsave -35 35 542 101 boxprim clip newpath +35 35 542 90 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.6905 set_scale +0.6136 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 577 136] /PAGES pdfmark +[ /CropBox [36 36 577 125] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Tactic_debug gsave 10 dict begin -167 18 48 18 ellipse_path +66 126 57 18 ellipse_path stroke gsave 10 dict begin -167 19 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext +66 121 moveto 93 -0.5 (Tactic_debug) alignedtext end grestore end grestore % Tacmach gsave 10 dict begin -298 72 36 18 ellipse_path +217 72 42 18 ellipse_path stroke gsave 10 dict begin -298 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext +217 67 moveto 63 -0.5 (Tacmach) alignedtext end grestore end grestore % Tactic_debug -> Tacmach -newpath 200 31 moveto -219 39 243 49 262 57 curveto +newpath 104 112 moveto +126 104 154 95 176 87 curveto stroke -newpath 262 54 moveto -270 60 lineto -260 59 lineto +0.000 0.000 0.000 edgecolor +newpath 174 85 moveto +184 84 lineto +176 90 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Refiner gsave 10 dict begin -411 99 31 18 ellipse_path +348 45 37 18 ellipse_path stroke gsave 10 dict begin -411 100 moveto (Refiner) 41 14.00 -0.50 alignedtext +348 40 moveto 53 -0.5 (Refiner) alignedtext end grestore end grestore % Tacmach -> Refiner -newpath 331 80 moveto -344 83 360 87 373 90 curveto +newpath 255 64 moveto +270 61 288 57 304 54 curveto stroke -newpath 373 87 moveto -382 92 lineto -372 92 lineto +0.000 0.000 0.000 edgecolor +newpath 303 52 moveto +313 52 lineto +304 57 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Logic gsave 10 dict begin -505 99 27 18 ellipse_path +452 45 30 18 ellipse_path stroke gsave 10 dict begin -505 100 moveto (Logic) 32 14.00 -0.50 alignedtext +452 40 moveto 38 -0.5 (Logic) alignedtext end grestore end grestore % Refiner -> Logic -newpath 442 99 moveto -450 99 459 99 468 99 curveto +newpath 386 45 moveto +395 45 404 45 412 45 curveto stroke -newpath 468 97 moveto -478 99 lineto -468 102 lineto +0.000 0.000 0.000 edgecolor +newpath 412 43 moveto +422 45 lineto +412 48 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Tacinterp +% Proof_trees gsave 10 dict begin -45 72 37 18 ellipse_path +569 45 51 18 ellipse_path stroke gsave 10 dict begin -45 73 moveto (Tacinterp) 53 14.00 -0.50 alignedtext +569 40 moveto 80 -0.5 (Proof_trees) alignedtext end grestore end grestore -% Tacinterp -> Tactic_debug -newpath 72 60 moveto -88 53 109 44 127 36 curveto +% Logic -> Proof_trees +newpath 482 45 moveto +490 45 499 45 508 45 curveto stroke -newpath 126 34 moveto -136 32 lineto -128 38 lineto +0.000 0.000 0.000 edgecolor +newpath 508 43 moveto +518 45 lineto +508 48 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Pfedit +% Proof_type gsave 10 dict begin -167 126 27 18 ellipse_path +707 45 50 18 ellipse_path stroke gsave 10 dict begin -167 127 moveto (Pfedit) 33 14.00 -0.50 alignedtext +707 40 moveto 79 -0.5 (Proof_type) alignedtext end grestore end grestore -% Tacinterp -> Pfedit -newpath 72 84 moveto -91 93 117 104 136 112 curveto -stroke -newpath 136 109 moveto -144 116 lineto -134 114 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Pfedit -> Tacmach -newpath 190 116 moveto -210 108 239 96 261 87 curveto -stroke -newpath 260 85 moveto -270 83 lineto -262 89 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Evar_refiner +% Tacexpr gsave 10 dict begin -298 126 45 18 ellipse_path +833 45 39 18 ellipse_path stroke gsave 10 dict begin -298 127 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext +833 40 moveto 56 -0.5 (Tacexpr) alignedtext end grestore end grestore -% Pfedit -> Evar_refiner -newpath 194 126 moveto -208 126 226 126 242 126 curveto +% Proof_type -> Tacexpr +newpath 758 45 moveto +767 45 775 45 784 45 curveto stroke -newpath 242 124 moveto -252 126 lineto -242 129 lineto +0.000 0.000 0.000 edgecolor +newpath 784 43 moveto +794 45 lineto +784 48 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Proof_trees +% Proof_trees -> Proof_type +newpath 620 45 moveto +629 45 637 45 646 45 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 646 43 moveto +656 45 lineto +646 48 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Pfedit gsave 10 dict begin -611 99 42 18 ellipse_path +66 18 31 18 ellipse_path stroke gsave 10 dict begin -611 100 moveto (Proof_trees) 64 14.00 -0.50 alignedtext +66 13 moveto 41 -0.5 (Pfedit) alignedtext end grestore end grestore -% Logic -> Proof_trees -newpath 532 99 moveto -540 99 549 99 558 99 curveto +% Pfedit -> Tacmach +newpath 93 28 moveto +115 36 149 48 175 57 curveto stroke -newpath 558 97 moveto -568 99 lineto -558 102 lineto +0.000 0.000 0.000 edgecolor +newpath 175 54 moveto +184 60 lineto +174 59 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Proof_type +% Evar_refiner gsave 10 dict begin -732 99 41 18 ellipse_path +217 18 56 18 ellipse_path stroke gsave 10 dict begin -732 100 moveto (Proof_type) 62 14.00 -0.50 alignedtext +217 13 moveto 91 -0.5 (Evar_refiner) alignedtext end grestore end grestore -% Proof_trees -> Proof_type -newpath 654 99 moveto -663 99 672 99 680 99 curveto +% Pfedit -> Evar_refiner +newpath 98 18 moveto +113 18 132 18 150 18 curveto stroke -newpath 680 97 moveto -690 99 lineto -680 102 lineto +0.000 0.000 0.000 edgecolor +newpath 150 16 moveto +160 18 lineto +150 21 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Evar_refiner -> Refiner -newpath 337 117 moveto -349 114 362 111 373 108 curveto +newpath 265 28 moveto +278 30 291 33 304 36 curveto stroke -newpath 372 106 moveto -382 106 lineto -373 111 lineto +0.000 0.000 0.000 edgecolor +newpath 304 33 moveto +313 38 lineto +303 38 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Clenv gsave 10 dict begin -167 72 27 18 ellipse_path +66 72 31 18 ellipse_path stroke gsave 10 dict begin -167 73 moveto (Clenv) 33 14.00 -0.50 alignedtext +66 67 moveto 40 -0.5 (Clenv) alignedtext end grestore end grestore % Clenv -> Tacmach -newpath 194 72 moveto -211 72 232 72 252 72 curveto +newpath 97 72 moveto +117 72 142 72 164 72 curveto stroke -newpath 252 70 moveto -262 72 lineto -252 75 lineto +0.000 0.000 0.000 edgecolor +newpath 164 70 moveto +174 72 lineto +164 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Clenv -> Evar_refiner -newpath 190 82 moveto -208 89 235 100 257 109 curveto +newpath 93 62 moveto +114 55 144 44 170 34 curveto stroke -newpath 258 107 moveto -266 113 lineto -256 111 lineto +0.000 0.000 0.000 edgecolor +newpath 169 32 moveto +179 31 lineto +170 37 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps index a628a56d9..16e85024d 100644 --- a/doc/tactics.dep.ps +++ b/doc/tactics.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (herbelin) Hugo Herbelin +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 577 125 +%%BoundingBox: 35 35 577 123 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,430 +225,466 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 577 125 +%%PageBoundingBox: 36 36 577 123 %%PageOrientation: Portrait gsave -35 35 542 90 boxprim clip newpath +35 35 542 88 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.4865 set_scale +0.4348 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 577 125] /PAGES pdfmark +[ /CropBox [36 36 577 123] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Termdn gsave 10 dict begin -939 18 32 18 ellipse_path +1091 180 39 18 ellipse_path stroke gsave 10 dict begin -939 19 moveto (Termdn) 44 14.00 -0.50 alignedtext +1091 175 moveto 56 -0.5 (Termdn) alignedtext end grestore end grestore % Dn gsave 10 dict begin -1057 18 27 18 ellipse_path +1207 180 27 18 ellipse_path stroke gsave 10 dict begin -1057 19 moveto (Dn) 17 14.00 -0.50 alignedtext +1207 175 moveto 21 -0.5 (Dn) alignedtext end grestore end grestore % Termdn -> Dn -newpath 972 18 moveto -987 18 1005 18 1021 18 curveto +newpath 1130 180 moveto +1143 180 1158 180 1171 180 curveto stroke -newpath 1020 16 moveto -1030 18 lineto -1020 21 lineto +0.000 0.000 0.000 edgecolor +newpath 1170 178 moveto +1180 180 lineto +1170 183 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Tactics gsave 10 dict begin -831 118 30 18 ellipse_path +830 86 34 18 ellipse_path stroke gsave 10 dict begin -831 119 moveto (Tactics) 40 14.00 -0.50 alignedtext +830 81 moveto 46 -0.5 (Tactics) alignedtext end grestore end grestore % Hipattern gsave 10 dict begin -939 149 36 18 ellipse_path +958 113 44 18 ellipse_path stroke gsave 10 dict begin -939 150 moveto (Hipattern) 52 14.00 -0.50 alignedtext +958 108 moveto 66 -0.5 (Hipattern) alignedtext end grestore end grestore % Tactics -> Hipattern -newpath 859 126 moveto -871 129 885 133 898 137 curveto +newpath 862 93 moveto +876 96 894 100 909 103 curveto stroke -newpath 898 134 moveto -907 140 lineto -897 139 lineto +0.000 0.000 0.000 edgecolor +newpath 910 101 moveto +919 105 lineto +909 105 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Tacticals gsave 10 dict begin -939 95 35 18 ellipse_path +958 59 40 18 ellipse_path stroke gsave 10 dict begin -939 96 moveto (Tacticals) 50 14.00 -0.50 alignedtext +958 54 moveto 58 -0.5 (Tacticals) alignedtext end grestore end grestore % Tactics -> Tacticals -newpath 860 112 moveto -871 110 884 107 896 104 curveto +newpath 862 79 moveto +877 76 896 72 912 69 curveto stroke -newpath 896 102 moveto -906 102 lineto -897 106 lineto +0.000 0.000 0.000 edgecolor +newpath 912 67 moveto +922 67 lineto +913 71 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Wcclausenv gsave 10 dict begin -1057 95 44 18 ellipse_path +1091 59 52 18 ellipse_path stroke gsave 10 dict begin -1057 96 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext +1091 54 moveto 83 -0.5 (Wcclausenv) alignedtext end grestore end grestore % Tacticals -> Wcclausenv -newpath 975 95 moveto -984 95 993 95 1002 95 curveto +newpath 998 59 moveto +1008 59 1018 59 1028 59 curveto stroke -newpath 1002 93 moveto -1012 95 lineto -1002 98 lineto +0.000 0.000 0.000 edgecolor +newpath 1028 57 moveto +1038 59 lineto +1028 62 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Tacentries +% Tacinterp gsave 10 dict begin -720 164 39 18 ellipse_path +439 18 43 18 ellipse_path stroke gsave 10 dict begin -720 165 moveto (Tacentries) 58 14.00 -0.50 alignedtext +439 13 moveto 65 -0.5 (Tacinterp) alignedtext end grestore end grestore -% Tacentries -> Tactics -newpath 749 152 moveto -764 146 782 138 797 132 curveto -stroke -newpath 796 130 moveto -806 128 lineto -798 134 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Setoid_replace +% Auto gsave 10 dict begin -388 110 52 18 ellipse_path +565 72 28 18 ellipse_path stroke gsave 10 dict begin -388 111 moveto (Setoid_replace) 83 14.00 -0.50 alignedtext +565 67 moveto 35 -0.5 (Auto) alignedtext end grestore end grestore -% Auto +% Tacinterp -> Auto +newpath 470 31 moveto +489 39 514 50 533 58 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 533 55 moveto +541 62 lineto +531 60 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Elim gsave 10 dict begin -503 110 27 18 ellipse_path +565 18 27 18 ellipse_path stroke gsave 10 dict begin -503 111 moveto (Auto) 28 14.00 -0.50 alignedtext +565 13 moveto 33 -0.5 (Elim) alignedtext end grestore end grestore -% Setoid_replace -> Auto -newpath 440 110 moveto -449 110 458 110 466 110 curveto +% Tacinterp -> Elim +newpath 483 18 moveto +498 18 514 18 528 18 curveto stroke -newpath 466 108 moveto -476 110 lineto -466 113 lineto +0.000 0.000 0.000 edgecolor +newpath 527 16 moveto +537 18 lineto +527 21 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Hiddentac gsave 10 dict begin -605 164 39 18 ellipse_path +688 18 46 18 ellipse_path stroke gsave 10 dict begin -605 165 moveto (Hiddentac) 57 14.00 -0.50 alignedtext +688 13 moveto 70 -0.5 (Hiddentac) alignedtext end grestore end grestore % Auto -> Hiddentac -newpath 525 121 moveto -538 129 556 138 571 146 curveto +newpath 588 62 moveto +605 54 629 44 648 36 curveto stroke -newpath 572 144 moveto -580 150 lineto -570 148 lineto +0.000 0.000 0.000 edgecolor +newpath 647 34 moveto +657 32 lineto +649 38 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Dhyp gsave 10 dict begin -605 110 27 18 ellipse_path +688 180 30 18 ellipse_path stroke gsave 10 dict begin -605 111 moveto (Dhyp) 31 14.00 -0.50 alignedtext +688 175 moveto 39 -0.5 (Dhyp) alignedtext end grestore end grestore % Auto -> Dhyp -newpath 530 110 moveto -542 110 556 110 568 110 curveto +newpath 578 88 moveto +597 112 630 152 630 153 curveto +637 158 646 163 653 167 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 654 165 moveto +662 171 lineto +652 169 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Elim -> Hiddentac +newpath 593 18 moveto +604 18 618 18 632 18 curveto stroke -newpath 568 108 moveto -578 110 lineto -568 113 lineto +0.000 0.000 0.000 edgecolor +newpath 632 16 moveto +642 18 lineto +632 21 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Setoid_replace +gsave 10 dict begin +439 72 60 18 ellipse_path +stroke +gsave 10 dict begin +439 67 moveto 99 -0.5 (Setoid_replace) alignedtext +end grestore +end grestore + +% Setoid_replace -> Auto +newpath 500 72 moveto +509 72 518 72 527 72 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 526 70 moveto +536 72 lineto +526 75 lineto +closepath +fill +0.000 0.000 0.000 edgecolor % Refine gsave 10 dict begin -720 72 29 18 ellipse_path +688 126 34 18 ellipse_path stroke gsave 10 dict begin -720 73 moveto (Refine) 37 14.00 -0.50 alignedtext +688 121 moveto 47 -0.5 (Refine) alignedtext end grestore end grestore % Refine -> Tactics -newpath 744 82 moveto -759 89 780 97 797 104 curveto +newpath 718 117 moveto +739 112 768 103 791 97 curveto stroke -newpath 798 102 moveto -806 108 lineto -796 106 lineto +0.000 0.000 0.000 edgecolor +newpath 790 95 moveto +800 95 lineto +791 100 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Nbtermdn gsave 10 dict begin -720 18 38 18 ellipse_path +830 180 47 18 ellipse_path stroke gsave 10 dict begin -720 19 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext +830 175 moveto 73 -0.5 (Nbtermdn) alignedtext end grestore end grestore % Btermdn gsave 10 dict begin -831 18 35 18 ellipse_path +958 180 42 18 ellipse_path stroke gsave 10 dict begin -831 19 moveto (Btermdn) 49 14.00 -0.50 alignedtext +958 175 moveto 62 -0.5 (Btermdn) alignedtext end grestore end grestore % Nbtermdn -> Btermdn -newpath 759 18 moveto -768 18 777 18 786 18 curveto +newpath 878 180 moveto +887 180 897 180 906 180 curveto stroke -newpath 786 16 moveto -796 18 lineto -786 21 lineto +0.000 0.000 0.000 edgecolor +newpath 906 178 moveto +916 180 lineto +906 183 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Btermdn -> Termdn -newpath 866 18 moveto -876 18 887 18 897 18 curveto +newpath 1000 180 moveto +1014 180 1029 180 1042 180 curveto stroke -newpath 896 16 moveto -906 18 lineto -896 21 lineto +0.000 0.000 0.000 edgecolor +newpath 1042 178 moveto +1052 180 lineto +1042 183 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Leminv gsave 10 dict begin -40 164 32 18 ellipse_path +46 72 38 18 ellipse_path stroke gsave 10 dict begin -40 165 moveto (Leminv) 43 14.00 -0.50 alignedtext +46 67 moveto 54 -0.5 (Leminv) alignedtext end grestore end grestore % Inv gsave 10 dict begin -152 164 27 18 ellipse_path +173 72 27 18 ellipse_path stroke gsave 10 dict begin -152 165 moveto (Inv) 18 14.00 -0.50 alignedtext +173 67 moveto 23 -0.5 (Inv) alignedtext end grestore end grestore % Leminv -> Inv -newpath 72 164 moveto -86 164 102 164 116 164 curveto -stroke -newpath 115 162 moveto -125 164 lineto -115 167 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Elim -gsave 10 dict begin -503 164 27 18 ellipse_path -stroke -gsave 10 dict begin -503 165 moveto (Elim) 27 14.00 -0.50 alignedtext -end grestore -end grestore - -% Inv -> Elim -newpath 179 164 moveto -242 164 396 164 467 164 curveto +newpath 84 72 moveto +101 72 120 72 137 72 curveto stroke -newpath 466 162 moveto -476 164 lineto -466 167 lineto +0.000 0.000 0.000 edgecolor +newpath 136 70 moveto +146 72 lineto +136 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Equality gsave 10 dict begin -266 110 34 18 ellipse_path +302 45 40 18 ellipse_path stroke gsave 10 dict begin -266 111 moveto (Equality) 47 14.00 -0.50 alignedtext +302 40 moveto 58 -0.5 (Equality) alignedtext end grestore end grestore % Inv -> Equality -newpath 174 153 moveto -190 145 213 134 231 126 curveto +newpath 199 67 moveto +215 64 236 59 255 55 curveto stroke -newpath 230 124 moveto -240 122 lineto -232 128 lineto +0.000 0.000 0.000 edgecolor +newpath 255 53 moveto +265 53 lineto +256 57 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Elim -> Hiddentac -newpath 530 164 moveto -538 164 547 164 556 164 curveto +% Equality -> Tacinterp +newpath 339 38 moveto +355 35 374 31 391 28 curveto stroke -newpath 556 162 moveto -566 164 lineto -556 167 lineto +0.000 0.000 0.000 edgecolor +newpath 390 26 moveto +400 26 lineto +391 31 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Equality -> Setoid_replace -newpath 300 110 moveto -308 110 317 110 326 110 curveto +newpath 339 52 moveto +352 55 367 58 382 61 curveto stroke -newpath 326 108 moveto -336 110 lineto -326 113 lineto +0.000 0.000 0.000 edgecolor +newpath 379 58 moveto +389 62 lineto +379 63 lineto closepath -gsave 0 setgray stroke grestore fill - -% Hiddentac -> Tacentries -newpath 644 164 moveto -653 164 662 164 670 164 curveto -stroke -newpath 670 162 moveto -680 164 lineto -670 167 lineto +fill +0.000 0.000 0.000 edgecolor + +% Hiddentac -> Tactics +newpath 718 32 moveto +732 39 746 45 746 45 curveto +751 48 776 60 798 71 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 797 68 moveto +805 74 lineto +795 72 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Eqdecide -gsave 10 dict begin -152 110 36 18 ellipse_path -stroke -gsave 10 dict begin -152 111 moveto (Eqdecide) 51 14.00 -0.50 alignedtext -end grestore -end grestore +% Dhyp -> Tactics +newpath 713 170 moveto +724 165 736 159 746 153 curveto +768 139 790 121 807 107 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 804 106 moveto +813 102 lineto +807 110 lineto +closepath +fill +0.000 0.000 0.000 edgecolor -% Eqdecide -> Equality -newpath 189 110 moveto -200 110 211 110 222 110 curveto +% Dhyp -> Nbtermdn +newpath 719 180 moveto +735 180 755 180 772 180 curveto stroke -newpath 222 108 moveto -232 110 lineto -222 113 lineto +0.000 0.000 0.000 edgecolor +newpath 772 178 moveto +782 180 lineto +772 183 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Eauto +% Contradiction gsave 10 dict begin -388 56 27 18 ellipse_path +688 72 57 18 ellipse_path stroke gsave 10 dict begin -388 57 moveto (Eauto) 32 14.00 -0.50 alignedtext +688 67 moveto 93 -0.5 (Contradiction) alignedtext end grestore end grestore -% Eauto -> Auto -newpath 410 66 moveto -428 75 453 86 473 95 curveto -stroke -newpath 473 92 moveto -481 99 lineto -471 97 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Dhyp -> Tactics -newpath 632 111 moveto -671 112 745 115 791 117 curveto -stroke -newpath 790 115 moveto -800 117 lineto -790 120 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Dhyp -> Nbtermdn -newpath 621 95 moveto -638 80 663 56 680 42 curveto -682 41 684 39 686 38 curveto +% Contradiction -> Tactics +newpath 743 77 moveto +758 79 773 80 787 81 curveto stroke -newpath 685 35 moveto -695 32 lineto -688 40 lineto +0.000 0.000 0.000 edgecolor +newpath 786 78 moveto +796 82 lineto +786 83 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Autorewrite gsave 10 dict begin -152 56 44 18 ellipse_path +173 18 53 18 ellipse_path stroke gsave 10 dict begin -152 57 moveto (Autorewrite) 67 14.00 -0.50 alignedtext +173 13 moveto 84 -0.5 (Autorewrite) alignedtext end grestore end grestore % Autorewrite -> Equality -newpath 181 70 moveto -196 78 216 87 232 94 curveto +newpath 218 28 moveto +231 30 244 33 256 35 curveto stroke -newpath 233 92 moveto -241 98 lineto -231 96 lineto +0.000 0.000 0.000 edgecolor +newpath 256 32 moveto +265 37 lineto +255 37 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps index 9679cb66f..216b70bd5 100644 --- a/doc/toplevel.dep.ps +++ b/doc/toplevel.dep.ps @@ -1,15 +1,96 @@ %!PS-Adobe-2.0 -%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001) -%%For: (herbelin) Hugo Herbelin +%%Creator: dot version 1.7.16 (Wed Feb 6 02:14:52 MST 2002) +%%For: (filliatr) Jean-Christophe Filliatre %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 256 +%%BoundingBox: 35 35 577 180 %%EndComments -%%BeginProlog save +%%BeginProlog /DotDict 200 dict def DotDict begin +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + %%BeginResource: procset /coord-font-family /Times-Roman def /default-font-family /Times-Roman def @@ -58,19 +139,15 @@ DotDict begin } def % draw aligned label in bounding box aligned to current point -% alignfactor tells what fraction to place on the left. -% -.5 is centered. -/alignedtext { % text labelwidth fontsz alignfactor - /alignfactor exch def - /fontsz exch def - /width exch def +/alignedtext { % width adj text /text exch def + /adj exch def + /width exch def gsave - % even if node or edge is dashed, don't paint text with dashes + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if [] 0 setdash - currentpoint newpath moveto - text stringwidth pop - alignfactor mul fontsz -.3 mul rmoveto text show grestore } def @@ -131,6 +208,7 @@ def /curlayer 0 def +%%EndResource %%EndProlog %%BeginSetup 14 default-font-family set_font @@ -147,423 +225,492 @@ def userdict (>>) cvn ([) cvn load put } if -%%EndResource %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 256 +%%PageBoundingBox: 36 36 577 180 %%PageOrientation: Portrait gsave -35 35 541 221 boxprim clip newpath +35 35 542 145 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.6236 set_scale +0.4180 set_scale 0 0 translate 0 rotate -[ /CropBox [36 36 576 256] /PAGES pdfmark +[ /CropBox [36 36 577 180] /PAGES pdfmark 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font -% Vernac -gsave 10 dict begin -542 126 30 18 ellipse_path -stroke -gsave 10 dict begin -542 127 moveto (Vernac) 40 14.00 -0.50 alignedtext -end grestore -end grestore - % Vernacinterp gsave 10 dict begin -695 118 46 18 ellipse_path +947 135 56 18 ellipse_path stroke gsave 10 dict begin -695 119 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext +947 130 moveto 91 -0.5 (Vernacinterp) alignedtext end grestore end grestore -% Vernac -> Vernacinterp -newpath 573 124 moveto -592 123 619 122 642 121 curveto -stroke -newpath 639 119 moveto -649 120 lineto -639 124 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Command +% Himsg gsave 10 dict begin -818 155 39 18 ellipse_path +1092 60 33 18 ellipse_path stroke gsave 10 dict begin -818 156 moveto (Command) 58 14.00 -0.50 alignedtext +1092 55 moveto 45 -0.5 (Himsg) alignedtext end grestore end grestore -% Vernacinterp -> Command -newpath 732 129 moveto -746 133 761 138 776 142 curveto -stroke -newpath 776 139 moveto -785 145 lineto -775 144 lineto +% Vernacinterp -> Himsg +newpath 979 120 moveto +991 114 1003 109 1004 108 curveto +1015 103 1042 88 1063 76 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1059 75 moveto +1069 73 lineto +1061 80 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Himsg +% Vernacexpr gsave 10 dict begin -818 78 29 18 ellipse_path +1232 179 51 18 ellipse_path stroke gsave 10 dict begin -818 79 moveto (Himsg) 37 14.00 -0.50 alignedtext +1232 174 moveto 81 -0.5 (Vernacexpr) alignedtext end grestore end grestore -% Vernacinterp -> Himsg -newpath 731 106 moveto -748 101 768 94 784 89 curveto +% Vernacinterp -> Vernacexpr +newpath 1002 139 moveto +1056 143 1131 149 1144 152 curveto +1159 154 1173 159 1187 163 curveto stroke -newpath 782 87 moveto -792 86 lineto -784 92 lineto +0.000 0.000 0.000 edgecolor +newpath 1187 160 moveto +1196 166 lineto +1186 165 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Vernacentries gsave 10 dict begin -542 226 49 18 ellipse_path +795 158 58 18 ellipse_path stroke gsave 10 dict begin -542 227 moveto (Vernacentries) 77 14.00 -0.50 alignedtext +795 153 moveto 95 -0.5 (Vernacentries) alignedtext end grestore end grestore % Vernacentries -> Vernacinterp -newpath 562 209 moveto -586 190 624 159 648 142 curveto -651 140 655 137 660 135 curveto +newpath 848 150 moveto +860 148 873 146 886 144 curveto stroke -newpath 656 134 moveto -666 132 lineto -658 139 lineto +0.000 0.000 0.000 edgecolor +newpath 886 142 moveto +896 143 lineto +886 146 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Discharge gsave 10 dict begin -695 280 38 18 ellipse_path +947 287 45 18 ellipse_path stroke gsave 10 dict begin -695 281 moveto (Discharge) 56 14.00 -0.50 alignedtext +947 282 moveto 68 -0.5 (Discharge) alignedtext end grestore end grestore % Vernacentries -> Discharge -newpath 577 239 moveto -601 247 631 257 656 266 curveto -stroke -newpath 656 263 moveto -664 269 lineto -654 268 lineto +newpath 809 176 moveto +826 197 857 233 890 258 curveto +895 262 902 266 908 269 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 909 267 moveto +917 273 lineto +907 271 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Metasyntax gsave 10 dict begin -695 226 43 18 ellipse_path +1092 179 51 18 ellipse_path stroke gsave 10 dict begin -695 227 moveto (Metasyntax) 65 14.00 -0.50 alignedtext +1092 174 moveto 81 -0.5 (Metasyntax) alignedtext end grestore end grestore % Vernacentries -> Metasyntax -newpath 591 226 moveto -608 226 626 226 642 226 curveto +newpath 852 162 moveto +903 166 978 171 1030 174 curveto stroke -newpath 642 224 moveto -652 226 lineto -642 229 lineto +0.000 0.000 0.000 edgecolor +newpath 1031 172 moveto +1041 175 lineto +1031 177 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Mltop gsave 10 dict begin -695 334 27 18 ellipse_path +947 81 32 18 ellipse_path stroke gsave 10 dict begin -695 335 moveto (Mltop) 34 14.00 -0.50 alignedtext +947 76 moveto 42 -0.5 (Mltop) alignedtext end grestore end grestore % Vernacentries -> Mltop -newpath 562 243 moveto -586 262 624 293 648 310 curveto -653 313 659 317 666 320 curveto -stroke -newpath 664 316 moveto -672 323 lineto -662 321 lineto +newpath 825 142 moveto +848 130 878 114 890 108 curveto +895 106 905 101 915 96 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 912 95 moveto +922 93 lineto +914 99 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Record gsave 10 dict begin -695 172 30 18 ellipse_path +947 231 35 18 ellipse_path stroke gsave 10 dict begin -695 173 moveto (Record) 40 14.00 -0.50 alignedtext +947 226 moveto 49 -0.5 (Record) alignedtext end grestore end grestore % Vernacentries -> Record -newpath 577 213 moveto -602 205 636 193 661 184 curveto +newpath 827 173 moveto +851 186 886 202 913 214 curveto stroke -newpath 659 182 moveto -669 181 lineto -661 187 lineto +0.000 0.000 0.000 edgecolor +newpath 913 211 moveto +921 218 lineto +911 216 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Class gsave 10 dict begin -818 220 27 18 ellipse_path +1232 283 28 18 ellipse_path stroke gsave 10 dict begin -818 221 moveto (Class) 30 14.00 -0.50 alignedtext +1232 278 moveto 34 -0.5 (Class) alignedtext end grestore end grestore % Discharge -> Class -newpath 722 267 moveto -741 257 768 245 788 235 curveto -stroke -newpath 786 233 moveto -796 231 lineto -788 238 lineto +newpath 983 298 moveto +1004 305 1029 312 1040 314 curveto +1086 320 1099 321 1144 314 curveto +1155 312 1179 304 1198 296 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1198 293 moveto +1208 292 lineto +1200 298 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Recordobj gsave 10 dict begin -818 280 39 18 ellipse_path +1092 287 47 18 ellipse_path stroke gsave 10 dict begin -818 281 moveto (Recordobj) 58 14.00 -0.50 alignedtext +1092 282 moveto 72 -0.5 (Recordobj) alignedtext end grestore end grestore % Discharge -> Recordobj -newpath 734 280 moveto -745 280 757 280 768 280 curveto +newpath 992 287 moveto +1006 287 1021 287 1035 287 curveto stroke -newpath 768 278 moveto -778 280 lineto -768 283 lineto +0.000 0.000 0.000 edgecolor +newpath 1035 285 moveto +1045 287 lineto +1035 290 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Record -> Command -newpath 725 168 moveto -738 166 755 164 770 162 curveto +% Metasyntax -> Vernacexpr +newpath 1144 179 moveto +1153 179 1161 179 1170 179 curveto stroke -newpath 770 160 moveto -780 160 lineto -771 164 lineto +0.000 0.000 0.000 edgecolor +newpath 1170 177 moveto +1180 179 lineto +1170 182 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Command +gsave 10 dict begin +1092 233 47 18 ellipse_path +stroke +gsave 10 dict begin +1092 228 moveto 73 -0.5 (Command) alignedtext +end grestore +end grestore -% Record -> Class -newpath 720 182 moveto -739 189 765 199 786 207 curveto +% Record -> Command +newpath 983 231 moveto +999 231 1017 232 1034 232 curveto stroke -newpath 786 204 moveto -794 211 lineto -784 209 lineto +0.000 0.000 0.000 edgecolor +newpath 1034 230 moveto +1044 232 lineto +1034 235 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Toplevel +% Vernac gsave 10 dict begin -247 199 35 18 ellipse_path +614 145 36 18 ellipse_path stroke gsave 10 dict begin -247 200 moveto (Toplevel) 49 14.00 -0.50 alignedtext +614 140 moveto 50 -0.5 (Vernac) alignedtext end grestore end grestore -% Toplevel -> Mltop -newpath 277 208 moveto -359 233 579 299 663 324 curveto +% Vernac -> Vernacentries +newpath 650 148 moveto +672 149 701 151 728 153 curveto stroke -newpath 661 321 moveto -670 326 lineto -660 326 lineto +0.000 0.000 0.000 edgecolor +newpath 728 151 moveto +738 154 lineto +728 155 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor + +% Toplevel +gsave 10 dict begin +275 72 40 18 ellipse_path +stroke +gsave 10 dict begin +275 67 moveto 59 -0.5 (Toplevel) alignedtext +end grestore +end grestore % Protectedtoplevel gsave 10 dict begin -377 99 59 18 ellipse_path +422 72 69 18 ellipse_path stroke gsave 10 dict begin -377 100 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext +422 67 moveto 117 -0.5 (Protectedtoplevel) alignedtext end grestore end grestore % Toplevel -> Protectedtoplevel -newpath 266 184 moveto -288 168 322 141 347 122 curveto +newpath 316 72 moveto +324 72 333 72 342 72 curveto stroke -newpath 346 120 moveto -355 116 lineto -349 124 lineto +0.000 0.000 0.000 edgecolor +newpath 342 70 moveto +352 72 lineto +342 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Protectedtoplevel -> Vernac -newpath 429 108 moveto -454 112 481 116 503 120 curveto +newpath 461 87 moveto +496 100 545 118 578 131 curveto stroke -newpath 502 117 moveto -512 121 lineto -502 122 lineto +0.000 0.000 0.000 edgecolor +newpath 577 128 moveto +585 134 lineto +575 132 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Cerrors gsave 10 dict begin -542 72 31 18 ellipse_path +795 42 36 18 ellipse_path stroke gsave 10 dict begin -542 73 moveto (Cerrors) 41 14.00 -0.50 alignedtext +795 37 moveto 51 -0.5 (Cerrors) alignedtext end grestore end grestore % Protectedtoplevel -> Cerrors -newpath 429 90 moveto -454 86 481 82 503 78 curveto -stroke -newpath 502 76 moveto -512 77 lineto -502 81 lineto +newpath 490 68 moveto +547 65 629 60 700 53 curveto +717 52 735 50 751 48 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 750 46 moveto +760 47 lineto +750 51 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Line_oriented_parser gsave 10 dict begin -542 18 70 18 ellipse_path +614 26 85 18 ellipse_path stroke gsave 10 dict begin -542 19 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext +614 21 moveto 149 -0.5 (Line_oriented_parser) alignedtext end grestore end grestore % Protectedtoplevel -> Line_oriented_parser -newpath 403 83 moveto -424 70 453 52 472 42 curveto -477 40 484 37 491 34 curveto +newpath 473 60 moveto +496 55 524 48 548 42 curveto stroke -newpath 488 32 moveto -498 32 lineto -489 37 lineto +0.000 0.000 0.000 edgecolor +newpath 547 40 moveto +557 40 lineto +548 45 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor -% Cerrors -> Himsg -newpath 573 73 moveto -625 74 726 76 782 77 curveto +% Command -> Vernacexpr +newpath 1126 220 moveto +1144 213 1168 204 1188 196 curveto stroke -newpath 779 75 moveto -789 77 lineto -779 80 lineto +0.000 0.000 0.000 edgecolor +newpath 1187 194 moveto +1197 192 lineto +1189 198 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Command -> Class +newpath 1127 245 moveto +1149 253 1177 263 1199 271 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1199 268 moveto +1207 274 lineto +1197 273 lineto +closepath +fill +0.000 0.000 0.000 edgecolor + +% Cerrors -> Himsg +newpath 832 44 moveto +882 47 972 53 1004 54 curveto +1019 55 1035 56 1049 57 curveto +stroke +0.000 0.000 0.000 edgecolor +newpath 1049 55 moveto +1059 58 lineto +1049 59 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Minicoq gsave 10 dict begin -42 253 34 18 ellipse_path +48 126 39 18 ellipse_path stroke gsave 10 dict begin -42 254 moveto (Minicoq) 47 14.00 -0.50 alignedtext +48 121 moveto 57 -0.5 (Minicoq) alignedtext end grestore end grestore % Fhimsg gsave 10 dict begin -144 253 31 18 ellipse_path +161 126 36 18 ellipse_path stroke gsave 10 dict begin -144 254 moveto (Fhimsg) 42 14.00 -0.50 alignedtext +161 121 moveto 51 -0.5 (Fhimsg) alignedtext end grestore end grestore % Minicoq -> Fhimsg -newpath 76 253 moveto -85 253 94 253 102 253 curveto +newpath 88 126 moveto +97 126 106 126 114 126 curveto stroke -newpath 102 251 moveto -112 253 lineto -102 256 lineto +0.000 0.000 0.000 edgecolor +newpath 114 124 moveto +124 126 lineto +114 129 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Coqtop gsave 10 dict begin -42 172 31 18 ellipse_path +48 45 36 18 ellipse_path stroke gsave 10 dict begin -42 173 moveto (Coqtop) 41 14.00 -0.50 alignedtext +48 40 moveto 50 -0.5 (Coqtop) alignedtext end grestore end grestore % Coqinit gsave 10 dict begin -144 199 31 18 ellipse_path +161 72 36 18 ellipse_path stroke gsave 10 dict begin -144 200 moveto (Coqinit) 42 14.00 -0.50 alignedtext +161 67 moveto 50 -0.5 (Coqinit) alignedtext end grestore end grestore % Coqtop -> Coqinit -newpath 70 180 moveto -81 183 94 186 106 189 curveto +newpath 81 53 moveto +93 56 106 59 118 62 curveto stroke -newpath 106 186 moveto -115 192 lineto -105 191 lineto +0.000 0.000 0.000 edgecolor +newpath 119 60 moveto +128 64 lineto +118 64 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Usage gsave 10 dict begin -144 145 27 18 ellipse_path +161 18 32 18 ellipse_path stroke gsave 10 dict begin -144 146 moveto (Usage) 34 14.00 -0.50 alignedtext +161 13 moveto 42 -0.5 (Usage) alignedtext end grestore end grestore % Coqtop -> Usage -newpath 70 164 moveto -82 161 96 157 109 154 curveto +newpath 81 37 moveto +94 34 109 31 122 27 curveto stroke -newpath 108 152 moveto -118 152 lineto -109 157 lineto +0.000 0.000 0.000 edgecolor +newpath 121 25 moveto +131 25 lineto +122 30 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor % Coqinit -> Toplevel -newpath 176 199 moveto -184 199 193 199 202 199 curveto +newpath 197 72 moveto +206 72 215 72 224 72 curveto stroke -newpath 202 197 moveto -212 199 lineto -202 202 lineto +0.000 0.000 0.000 edgecolor +newpath 224 70 moveto +234 72 lineto +224 75 lineto closepath -gsave 0 setgray stroke grestore fill +fill +0.000 0.000 0.000 edgecolor endpage grestore %%PageTrailer diff --git a/library/library.ml b/library/library.ml index 1f75b4ca0..64e127258 100644 --- a/library/library.ml +++ b/library/library.ml @@ -260,7 +260,7 @@ let open_libraries export modl = let compunit_cache = ref CompilingLibraryMap.empty -let vo_magic_number = 0703 (* V7.3 *) +let vo_magic_number = 0704 (* V7.4 *) let (raw_extern_library, raw_intern_library) = System.raw_extern_intern vo_magic_number ".vo" -- cgit v1.2.3