aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ANNONCE11
-rw-r--r--CHANGES4
-rw-r--r--INSTALL14
-rw-r--r--README4
-rw-r--r--README.win3
-rw-r--r--distrib/RH/coq.spec.tpl6
-rw-r--r--doc/kernel.dep.ps596
-rw-r--r--doc/library.dep.ps467
-rw-r--r--doc/parsing.dep.ps635
-rw-r--r--doc/pretyping.dep.ps719
-rw-r--r--doc/proofs.dep.ps345
-rw-r--r--doc/tactics.dep.ps582
-rw-r--r--doc/toplevel.dep.ps585
-rw-r--r--library/library.ml2
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"
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:52:46 +0000