aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-09 17:48:39 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-09 17:48:39 +0000
commit9fd56d7a7281edece40240d52d25b9144d12439e (patch)
treefb8ff8c57f1ff3695e95df9697de23def1c29db0
parent3cd1a988f93566579740294c7fafbfc81b174675 (diff)
MAJ après restructuration kernel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2180 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--doc/kernel.dep.ps302
-rw-r--r--doc/library.dep.ps258
-rw-r--r--doc/parsing.dep.ps365
-rw-r--r--doc/pretyping.dep.ps506
-rw-r--r--doc/proofs.dep.ps169
-rw-r--r--doc/tactics.dep.ps413
-rw-r--r--doc/toplevel.dep.ps375
7 files changed, 1329 insertions, 1059 deletions
diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 1dcc8f873..3672e35d4 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 91
+%%BoundingBox: 36 36 577 73
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,365 +131,319 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 91
+%%PageBoundingBox: 36 36 577 73
+%%PageOrientation: Portrait
gsave
-35 35 542 56 boxprim clip newpath
+35 35 542 38 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.3982 set_scale
+0.3953 set_scale
0 0 translate 0 rotate
+[ /CropBox [36 36 577 73] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Univ
gsave 10 dict begin
-1231 101 27 18 ellipse_path
+1233 74 27 18 ellipse_path
stroke
gsave 10 dict begin
-1231 102 moveto (Univ) 28 14.00 -0.50 alignedtext
+1233 75 moveto (Univ) 28 14.00 -0.50 alignedtext
end grestore
end grestore
% Names
gsave 10 dict begin
-1326 101 29 18 ellipse_path
+1328 74 29 18 ellipse_path
stroke
gsave 10 dict begin
-1326 102 moveto (Names) 38 14.00 -0.50 alignedtext
+1328 75 moveto (Names) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Univ -> Names
-newpath 1258 101 moveto
-1267 101 1277 101 1286 101 curveto
+newpath 1260 74 moveto
+1269 74 1279 74 1288 74 curveto
stroke
-newpath 1286 99 moveto
-1296 101 lineto
-1286 104 lineto
+newpath 1288 72 moveto
+1298 74 lineto
+1288 77 lineto
closepath
gsave 0 setgray stroke grestore fill
% Typeops
gsave 10 dict begin
-265 64 34 18 ellipse_path
+273 18 34 18 ellipse_path
stroke
gsave 10 dict begin
-265 65 moveto (Typeops) 48 14.00 -0.50 alignedtext
+273 19 moveto (Typeops) 48 14.00 -0.50 alignedtext
end grestore
end grestore
% Inductive
gsave 10 dict begin
-381 72 36 18 ellipse_path
+381 20 36 18 ellipse_path
stroke
gsave 10 dict begin
-381 73 moveto (Inductive) 52 14.00 -0.50 alignedtext
+381 21 moveto (Inductive) 52 14.00 -0.50 alignedtext
end grestore
end grestore
% Typeops -> Inductive
-newpath 299 66 moveto
-310 67 323 68 334 69 curveto
+newpath 308 19 moveto
+317 19 326 19 334 19 curveto
stroke
-newpath 334 67 moveto
-344 70 lineto
-334 71 lineto
+newpath 334 17 moveto
+344 19 lineto
+334 22 lineto
closepath
gsave 0 setgray stroke grestore fill
% Type_errors
gsave 10 dict begin
-381 18 44 18 ellipse_path
+499 24 44 18 ellipse_path
stroke
gsave 10 dict begin
-381 19 moveto (Type_errors) 68 14.00 -0.50 alignedtext
+499 25 moveto (Type_errors) 68 14.00 -0.50 alignedtext
end grestore
end grestore
-% Typeops -> Type_errors
-newpath 292 53 moveto
-306 47 324 41 340 35 curveto
+% Inductive -> Type_errors
+newpath 418 21 moveto
+426 21 435 22 444 22 curveto
stroke
-newpath 339 33 moveto
-349 31 lineto
-341 37 lineto
+newpath 444 20 moveto
+454 22 lineto
+444 25 lineto
closepath
gsave 0 setgray stroke grestore fill
% Reduction
gsave 10 dict begin
-501 72 39 18 ellipse_path
+619 47 39 18 ellipse_path
stroke
gsave 10 dict begin
-501 73 moveto (Reduction) 57 14.00 -0.50 alignedtext
+619 48 moveto (Reduction) 57 14.00 -0.50 alignedtext
end grestore
end grestore
-% Inductive -> Reduction
-newpath 418 72 moveto
-429 72 441 72 452 72 curveto
-stroke
-newpath 452 70 moveto
-462 72 lineto
-452 75 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
% Type_errors -> Reduction
-newpath 411 31 moveto
-427 39 448 48 465 55 curveto
+newpath 539 32 moveto
+550 34 562 36 573 38 curveto
stroke
-newpath 465 52 moveto
-473 59 lineto
-463 57 lineto
+newpath 574 36 moveto
+583 40 lineto
+573 40 lineto
closepath
gsave 0 setgray stroke grestore fill
% Closure
gsave 10 dict begin
-608 72 32 18 ellipse_path
+726 47 32 18 ellipse_path
stroke
gsave 10 dict begin
-608 73 moveto (Closure) 43 14.00 -0.50 alignedtext
+726 48 moveto (Closure) 43 14.00 -0.50 alignedtext
end grestore
end grestore
% Reduction -> Closure
-newpath 540 72 moveto
-549 72 558 72 566 72 curveto
+newpath 658 47 moveto
+667 47 676 47 684 47 curveto
stroke
-newpath 566 70 moveto
-576 72 lineto
-566 75 lineto
+newpath 684 45 moveto
+694 47 lineto
+684 50 lineto
closepath
gsave 0 setgray stroke grestore fill
% Term
gsave 10 dict begin
-1139 74 27 18 ellipse_path
+1141 47 27 18 ellipse_path
stroke
gsave 10 dict begin
-1139 75 moveto (Term) 30 14.00 -0.50 alignedtext
+1141 48 moveto (Term) 30 14.00 -0.50 alignedtext
end grestore
end grestore
% Term -> Univ
-newpath 1164 81 moveto
-1174 84 1186 88 1197 91 curveto
+newpath 1166 54 moveto
+1176 57 1188 61 1199 64 curveto
stroke
-newpath 1197 88 moveto
-1206 94 lineto
-1196 93 lineto
+newpath 1199 61 moveto
+1208 67 lineto
+1198 66 lineto
closepath
gsave 0 setgray stroke grestore fill
% Esubst
gsave 10 dict begin
-1231 47 29 18 ellipse_path
+1233 20 29 18 ellipse_path
stroke
gsave 10 dict begin
-1231 48 moveto (Esubst) 37 14.00 -0.50 alignedtext
+1233 21 moveto (Esubst) 37 14.00 -0.50 alignedtext
end grestore
end grestore
% Term -> Esubst
-newpath 1164 67 moveto
-1174 64 1185 61 1196 58 curveto
+newpath 1166 40 moveto
+1176 37 1187 34 1198 31 curveto
stroke
-newpath 1195 56 moveto
-1205 55 lineto
-1196 61 lineto
+newpath 1197 29 moveto
+1207 28 lineto
+1198 34 lineto
closepath
gsave 0 setgray stroke grestore fill
% Sign
gsave 10 dict begin
-1049 74 27 18 ellipse_path
+1051 47 27 18 ellipse_path
stroke
gsave 10 dict begin
-1049 75 moveto (Sign) 25 14.00 -0.50 alignedtext
+1051 48 moveto (Sign) 25 14.00 -0.50 alignedtext
end grestore
end grestore
% Sign -> Term
-newpath 1076 74 moveto
-1084 74 1093 74 1102 74 curveto
+newpath 1078 47 moveto
+1086 47 1095 47 1104 47 curveto
stroke
-newpath 1102 72 moveto
-1112 74 lineto
-1102 77 lineto
+newpath 1104 45 moveto
+1114 47 lineto
+1104 50 lineto
closepath
gsave 0 setgray stroke grestore fill
% Safe_typing
gsave 10 dict begin
-44 92 44 18 ellipse_path
+52 46 44 18 ellipse_path
stroke
gsave 10 dict begin
-44 93 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
+52 47 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
end grestore
end grestore
% Cooking
gsave 10 dict begin
-265 118 34 18 ellipse_path
+273 72 34 18 ellipse_path
stroke
gsave 10 dict begin
-265 119 moveto (Cooking) 48 14.00 -0.50 alignedtext
+273 73 moveto (Cooking) 48 14.00 -0.50 alignedtext
end grestore
end grestore
% Safe_typing -> Cooking
-newpath 86 97 moveto
-126 102 184 109 223 113 curveto
+newpath 94 51 moveto
+134 56 192 63 231 67 curveto
stroke
-newpath 221 110 moveto
-231 114 lineto
-221 115 lineto
+newpath 229 64 moveto
+239 68 lineto
+229 69 lineto
closepath
gsave 0 setgray stroke grestore fill
% Indtypes
gsave 10 dict begin
-159 68 34 18 ellipse_path
+167 22 34 18 ellipse_path
stroke
gsave 10 dict begin
-159 69 moveto (Indtypes) 48 14.00 -0.50 alignedtext
+167 23 moveto (Indtypes) 48 14.00 -0.50 alignedtext
end grestore
end grestore
% Safe_typing -> Indtypes
-newpath 83 84 moveto
-94 82 106 79 117 77 curveto
+newpath 91 38 moveto
+102 36 114 33 125 31 curveto
stroke
-newpath 117 75 moveto
-127 75 lineto
-118 79 lineto
+newpath 125 29 moveto
+135 29 lineto
+126 33 lineto
closepath
gsave 0 setgray stroke grestore fill
% Cooking -> Reduction
-newpath 300 116 moveto
-336 114 393 109 426 102 curveto
-437 99 453 94 468 88 curveto
+newpath 307 70 moveto
+369 65 500 56 571 51 curveto
stroke
-newpath 464 87 moveto
-474 85 lineto
-466 92 lineto
+newpath 570 49 moveto
+580 50 lineto
+570 54 lineto
closepath
gsave 0 setgray stroke grestore fill
% Indtypes -> Typeops
-newpath 193 67 moveto
-203 67 213 66 224 66 curveto
-stroke
-newpath 221 64 moveto
-231 66 lineto
-221 69 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Instantiate
-gsave 10 dict begin
-716 72 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-716 73 moveto (Instantiate) 58 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Closure -> Instantiate
-newpath 640 72 moveto
-648 72 657 72 666 72 curveto
+newpath 201 21 moveto
+211 21 221 20 232 20 curveto
stroke
-newpath 666 70 moveto
-676 72 lineto
-666 75 lineto
+newpath 229 18 moveto
+239 20 lineto
+229 23 lineto
closepath
gsave 0 setgray stroke grestore fill
% Environ
gsave 10 dict begin
-825 99 33 18 ellipse_path
-stroke
-gsave 10 dict begin
-825 100 moveto (Environ) 45 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Instantiate -> Environ
-newpath 751 81 moveto
-762 84 774 87 786 89 curveto
-stroke
-newpath 786 86 moveto
-795 92 lineto
-785 91 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Evd
-gsave 10 dict begin
-940 47 27 18 ellipse_path
+827 47 33 18 ellipse_path
stroke
gsave 10 dict begin
-940 48 moveto (Evd) 22 14.00 -0.50 alignedtext
+827 48 moveto (Environ) 45 14.00 -0.50 alignedtext
end grestore
end grestore
-% Instantiate -> Evd
-newpath 755 68 moveto
-797 63 864 56 905 51 curveto
+% Closure -> Environ
+newpath 758 47 moveto
+766 47 775 47 784 47 curveto
stroke
-newpath 903 49 moveto
-913 50 lineto
-903 54 lineto
+newpath 784 45 moveto
+794 47 lineto
+784 50 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declarations
gsave 10 dict begin
-940 101 45 18 ellipse_path
+942 47 45 18 ellipse_path
stroke
gsave 10 dict begin
-940 102 moveto (Declarations) 70 14.00 -0.50 alignedtext
+942 48 moveto (Declarations) 70 14.00 -0.50 alignedtext
end grestore
end grestore
% Environ -> Declarations
-newpath 858 100 moveto
-866 100 875 100 884 100 curveto
-stroke
-newpath 884 98 moveto
-894 100 lineto
-884 103 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Evd -> Sign
-newpath 966 53 moveto
-980 56 998 61 1015 65 curveto
+newpath 860 47 moveto
+868 47 877 47 886 47 curveto
stroke
-newpath 1015 62 moveto
-1024 68 lineto
-1014 67 lineto
+newpath 886 45 moveto
+896 47 lineto
+886 50 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declarations -> Sign
-newpath 979 91 moveto
-991 89 1003 86 1015 83 curveto
+newpath 988 47 moveto
+997 47 1006 47 1014 47 curveto
stroke
-newpath 1014 81 moveto
-1024 80 lineto
-1015 86 lineto
+newpath 1014 45 moveto
+1024 47 lineto
+1014 50 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index 7a5cdeed3..eb358f772 100644
--- a/doc/library.dep.ps
+++ b/doc/library.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 525 235
+%%BoundingBox: 36 36 543 235
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,239 +131,293 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 525 235
+%%PageBoundingBox: 36 36 543 235
+%%PageOrientation: Portrait
gsave
-35 35 490 200 boxprim clip newpath
+35 35 508 200 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0 0 translate 0 rotate
+[ /CropBox [36 36 543 235] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% States
gsave 10 dict begin
-32 180 27 18 ellipse_path
+40 126 27 18 ellipse_path
stroke
gsave 10 dict begin
-32 181 moveto (States) 33 14.00 -0.50 alignedtext
+40 127 moveto (States) 33 14.00 -0.50 alignedtext
end grestore
end grestore
% Library
gsave 10 dict begin
-136 180 31 18 ellipse_path
+144 126 31 18 ellipse_path
stroke
gsave 10 dict begin
-136 181 moveto (Library) 41 14.00 -0.50 alignedtext
+144 127 moveto (Library) 41 14.00 -0.50 alignedtext
end grestore
end grestore
% States -> Library
-newpath 59 180 moveto
-70 180 83 180 95 180 curveto
+newpath 67 126 moveto
+78 126 91 126 103 126 curveto
stroke
-newpath 95 178 moveto
-105 180 lineto
-95 183 lineto
+newpath 103 124 moveto
+113 126 lineto
+103 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Global
gsave 10 dict begin
-238 180 29 18 ellipse_path
+246 126 29 18 ellipse_path
stroke
gsave 10 dict begin
-238 181 moveto (Global) 38 14.00 -0.50 alignedtext
+246 127 moveto (Global) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Library -> Global
-newpath 167 180 moveto
-177 180 188 180 198 180 curveto
+newpath 175 126 moveto
+185 126 196 126 206 126 curveto
stroke
-newpath 198 178 moveto
-208 180 lineto
-198 183 lineto
+newpath 206 124 moveto
+216 126 lineto
+206 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Lib
gsave 10 dict begin
-238 126 27 18 ellipse_path
+246 72 27 18 ellipse_path
stroke
gsave 10 dict begin
-238 127 moveto (Lib) 19 14.00 -0.50 alignedtext
+246 73 moveto (Lib) 19 14.00 -0.50 alignedtext
end grestore
end grestore
% Library -> Lib
-newpath 159 168 moveto
-173 160 193 150 209 141 curveto
+newpath 167 114 moveto
+181 106 201 96 217 87 curveto
stroke
-newpath 207 139 moveto
-217 137 lineto
-209 144 lineto
+newpath 215 85 moveto
+225 83 lineto
+217 90 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Opaque
+gsave 10 dict begin
+144 180 32 18 ellipse_path
+stroke
+gsave 10 dict begin
+144 181 moveto (Opaque) 43 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Opaque -> Global
+newpath 167 168 moveto
+181 160 200 151 216 142 curveto
+stroke
+newpath 214 140 moveto
+224 138 lineto
+216 145 lineto
closepath
gsave 0 setgray stroke grestore fill
% Nametab
gsave 10 dict begin
-340 153 35 18 ellipse_path
+349 126 35 18 ellipse_path
stroke
gsave 10 dict begin
-340 154 moveto (Nametab) 50 14.00 -0.50 alignedtext
+349 127 moveto (Nametab) 50 14.00 -0.50 alignedtext
end grestore
end grestore
-% Libobject
+% Global -> Nametab
+newpath 276 126 moveto
+285 126 294 126 303 126 curveto
+stroke
+newpath 303 124 moveto
+313 126 lineto
+303 129 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Nameops
gsave 10 dict begin
-450 180 37 18 ellipse_path
+460 153 36 18 ellipse_path
stroke
gsave 10 dict begin
-450 181 moveto (Libobject) 53 14.00 -0.50 alignedtext
+460 154 moveto (Nameops) 52 14.00 -0.50 alignedtext
end grestore
end grestore
-% Nametab -> Libobject
-newpath 372 161 moveto
-383 163 396 166 408 169 curveto
+% Nametab -> Nameops
+newpath 381 134 moveto
+392 137 405 140 417 143 curveto
stroke
-newpath 408 166 moveto
-417 172 lineto
-407 171 lineto
+newpath 418 141 moveto
+427 145 lineto
+417 145 lineto
closepath
gsave 0 setgray stroke grestore fill
% Summary
gsave 10 dict begin
-450 126 37 18 ellipse_path
+460 99 37 18 ellipse_path
stroke
gsave 10 dict begin
-450 127 moveto (Summary) 54 14.00 -0.50 alignedtext
+460 100 moveto (Summary) 54 14.00 -0.50 alignedtext
end grestore
end grestore
% Nametab -> Summary
-newpath 372 145 moveto
-383 143 395 140 406 137 curveto
+newpath 381 118 moveto
+392 116 405 112 417 109 curveto
stroke
-newpath 406 134 moveto
-416 134 lineto
-407 139 lineto
+newpath 416 107 moveto
+426 107 lineto
+417 112 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Global -> Nametab
-newpath 265 173 moveto
-275 170 287 167 298 164 curveto
+% Lib -> Nametab
+newpath 267 83 moveto
+281 91 300 100 316 109 curveto
stroke
-newpath 298 161 moveto
-308 161 lineto
-299 166 lineto
+newpath 316 106 moveto
+324 113 lineto
+314 111 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Lib -> Nametab
-newpath 263 133 moveto
-274 136 287 139 299 142 curveto
+% Libobject
+gsave 10 dict begin
+349 72 37 18 ellipse_path
stroke
-newpath 299 139 moveto
-308 145 lineto
-298 144 lineto
+gsave 10 dict begin
+349 73 moveto (Libobject) 53 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Lib -> Libobject
+newpath 273 72 moveto
+282 72 292 72 302 72 curveto
+stroke
+newpath 302 70 moveto
+312 72 lineto
+302 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Impargs
gsave 10 dict begin
-136 126 33 18 ellipse_path
+144 72 33 18 ellipse_path
stroke
gsave 10 dict begin
-136 127 moveto (Impargs) 45 14.00 -0.50 alignedtext
+144 73 moveto (Impargs) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Impargs -> Global
-newpath 160 139 moveto
-174 147 192 156 207 164 curveto
+newpath 168 85 moveto
+182 93 200 102 215 110 curveto
stroke
-newpath 207 161 moveto
-215 168 lineto
-205 166 lineto
+newpath 215 107 moveto
+223 114 lineto
+213 112 lineto
closepath
gsave 0 setgray stroke grestore fill
% Impargs -> Lib
-newpath 169 126 moveto
-180 126 191 126 201 126 curveto
+newpath 177 72 moveto
+188 72 199 72 209 72 curveto
stroke
-newpath 201 124 moveto
-211 126 lineto
-201 129 lineto
+newpath 209 70 moveto
+219 72 lineto
+209 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Goptions
gsave 10 dict begin
-136 72 36 18 ellipse_path
+144 18 36 18 ellipse_path
stroke
gsave 10 dict begin
-136 73 moveto (Goptions) 51 14.00 -0.50 alignedtext
+144 19 moveto (Goptions) 51 14.00 -0.50 alignedtext
end grestore
end grestore
+% Goptions -> Global
+newpath 166 32 moveto
+172 35 176 38 180 42 curveto
+196 60 202 84 216 102 curveto
+217 103 218 104 219 105 curveto
+stroke
+newpath 221 104 moveto
+227 112 lineto
+218 107 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% Goptions -> Lib
-newpath 161 85 moveto
-175 93 193 102 209 111 curveto
+newpath 169 31 moveto
+183 39 201 48 217 57 curveto
stroke
-newpath 209 108 moveto
-217 115 lineto
-207 113 lineto
+newpath 217 54 moveto
+225 61 lineto
+215 59 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declare
gsave 10 dict begin
-32 72 32 18 ellipse_path
+40 72 32 18 ellipse_path
stroke
gsave 10 dict begin
-32 73 moveto (Declare) 43 14.00 -0.50 alignedtext
+40 73 moveto (Declare) 43 14.00 -0.50 alignedtext
end grestore
end grestore
-% Declare -> Impargs
-newpath 56 84 moveto
-70 92 88 101 104 110 curveto
+% Declare -> Library
+newpath 64 84 moveto
+78 92 97 101 113 110 curveto
stroke
-newpath 104 107 moveto
-112 114 lineto
-102 112 lineto
+newpath 113 107 moveto
+121 114 lineto
+111 112 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Indrec
-gsave 10 dict begin
-136 18 28 18 ellipse_path
-stroke
-gsave 10 dict begin
-136 19 moveto (Indrec) 35 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Declare -> Indrec
-newpath 56 60 moveto
-70 52 90 42 106 33 curveto
+% Declare -> Impargs
+newpath 72 72 moveto
+81 72 92 72 101 72 curveto
stroke
-newpath 104 31 moveto
-114 29 lineto
-106 36 lineto
+newpath 101 70 moveto
+111 72 lineto
+101 75 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 3507cf4a9..9df862840 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 576 186
+%%BoundingBox: 36 36 576 232
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,373 +131,398 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 576 186
+%%PageBoundingBox: 36 36 576 232
+%%PageOrientation: Portrait
gsave
-35 35 541 151 boxprim clip newpath
+35 35 541 197 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6818 set_scale
+0.7584 set_scale
0 0 translate 0 rotate
+[ /CropBox [36 36 576 232] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Pcoq
gsave 10 dict begin
-669 72 27 18 ellipse_path
+581 103 27 18 ellipse_path
stroke
gsave 10 dict begin
-669 73 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+581 104 moveto (Pcoq) 28 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqast
gsave 10 dict begin
-762 72 30 18 ellipse_path
+674 103 30 18 ellipse_path
stroke
gsave 10 dict begin
-762 73 moveto (Coqast) 38 14.00 -0.50 alignedtext
+674 104 moveto (Coqast) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Pcoq -> Coqast
-newpath 696 72 moveto
-704 72 713 72 722 72 curveto
+newpath 608 103 moveto
+616 103 625 103 634 103 curveto
stroke
-newpath 722 70 moveto
-732 72 lineto
-722 75 lineto
+newpath 634 101 moveto
+644 103 lineto
+634 106 lineto
closepath
gsave 0 setgray stroke grestore fill
% Extend
gsave 10 dict begin
-486 124 30 18 ellipse_path
+398 52 30 18 ellipse_path
stroke
gsave 10 dict begin
-486 125 moveto (Extend) 39 14.00 -0.50 alignedtext
+398 53 moveto (Extend) 39 14.00 -0.50 alignedtext
end grestore
end grestore
% Ast
gsave 10 dict begin
-579 72 27 18 ellipse_path
+491 103 27 18 ellipse_path
stroke
gsave 10 dict begin
-579 73 moveto (Ast) 19 14.00 -0.50 alignedtext
+491 104 moveto (Ast) 19 14.00 -0.50 alignedtext
end grestore
end grestore
% Extend -> Ast
-newpath 508 112 moveto
-520 105 536 96 550 88 curveto
+newpath 421 64 moveto
+433 71 448 79 462 86 curveto
stroke
-newpath 548 86 moveto
-558 84 lineto
-550 91 lineto
+newpath 463 84 moveto
+470 91 lineto
+460 88 lineto
closepath
gsave 0 setgray stroke grestore fill
% Ast -> Pcoq
-newpath 606 72 moveto
-614 72 623 72 632 72 curveto
+newpath 518 103 moveto
+526 103 535 103 544 103 curveto
stroke
-newpath 632 70 moveto
-642 72 lineto
-632 75 lineto
+newpath 544 101 moveto
+554 103 lineto
+544 106 lineto
closepath
gsave 0 setgray stroke grestore fill
% Termast
gsave 10 dict begin
-380 18 33 18 ellipse_path
+292 156 33 18 ellipse_path
stroke
gsave 10 dict begin
-380 19 moveto (Termast) 45 14.00 -0.50 alignedtext
+292 157 moveto (Termast) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Termast -> Ast
-newpath 413 22 moveto
-443 25 489 32 516 40 curveto
-526 43 540 50 553 57 curveto
+newpath 325 152 moveto
+355 149 401 143 428 136 curveto
+438 133 451 127 462 120 curveto
stroke
-newpath 551 53 moveto
-559 60 lineto
-549 58 lineto
+newpath 461 118 moveto
+471 115 lineto
+463 122 lineto
closepath
gsave 0 setgray stroke grestore fill
% Search
gsave 10 dict begin
-30 46 29 18 ellipse_path
+48 198 29 18 ellipse_path
stroke
gsave 10 dict begin
-30 47 moveto (Search) 37 14.00 -0.50 alignedtext
+48 199 moveto (Search) 37 14.00 -0.50 alignedtext
end grestore
end grestore
% Astterm
gsave 10 dict begin
-258 72 33 18 ellipse_path
+170 94 33 18 ellipse_path
stroke
gsave 10 dict begin
-258 73 moveto (Astterm) 45 14.00 -0.50 alignedtext
+170 95 moveto (Astterm) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Search -> Astterm
-newpath 59 49 moveto
-99 54 171 62 216 67 curveto
-stroke
-newpath 215 64 moveto
-225 68 lineto
-215 69 lineto
+newpath 71 186 moveto
+78 183 84 178 88 174 curveto
+104 157 109 133 124 118 curveto
+127 115 132 112 137 109 curveto
+stroke
+newpath 134 108 moveto
+144 106 lineto
+136 112 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Pretty
+% Coqlib
gsave 10 dict begin
-136 22 27 18 ellipse_path
+292 229 29 18 ellipse_path
stroke
gsave 10 dict begin
-136 23 moveto (Pretty) 33 14.00 -0.50 alignedtext
+292 230 moveto (Coqlib) 38 14.00 -0.50 alignedtext
end grestore
end grestore
-% Search -> Pretty
-newpath 58 40 moveto
-71 37 87 33 101 30 curveto
-stroke
-newpath 100 28 moveto
-110 28 lineto
-101 33 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Astterm -> Termast
-newpath 284 61 moveto
-302 53 327 42 346 34 curveto
+% Search -> Coqlib
+newpath 70 210 moveto
+87 218 109 229 124 232 curveto
+159 239 217 235 255 233 curveto
stroke
-newpath 344 32 moveto
-354 30 lineto
-346 37 lineto
+newpath 253 231 moveto
+263 232 lineto
+253 236 lineto
closepath
gsave 0 setgray stroke grestore fill
% Printer
gsave 10 dict begin
-258 18 29 18 ellipse_path
+170 148 29 18 ellipse_path
stroke
gsave 10 dict begin
-258 19 moveto (Printer) 38 14.00 -0.50 alignedtext
+170 149 moveto (Printer) 38 14.00 -0.50 alignedtext
end grestore
end grestore
-% Pretty -> Printer
-newpath 163 21 moveto
-179 20 200 20 218 19 curveto
+% Search -> Printer
+newpath 73 188 moveto
+91 180 116 170 137 162 curveto
+stroke
+newpath 135 160 moveto
+145 158 lineto
+137 165 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Astterm -> Termast
+newpath 194 106 moveto
+213 116 239 129 260 139 curveto
stroke
-newpath 218 17 moveto
-228 19 lineto
-218 22 lineto
+newpath 260 136 moveto
+268 143 lineto
+258 141 lineto
closepath
gsave 0 setgray stroke grestore fill
% Printer -> Termast
-newpath 288 18 moveto
-303 18 321 18 337 18 curveto
+newpath 200 150 moveto
+215 151 233 152 249 153 curveto
stroke
-newpath 337 16 moveto
-347 18 lineto
-337 21 lineto
+newpath 249 151 moveto
+259 154 lineto
+249 155 lineto
closepath
gsave 0 setgray stroke grestore fill
% Esyntax
gsave 10 dict begin
-380 180 33 18 ellipse_path
+292 48 33 18 ellipse_path
stroke
gsave 10 dict begin
-380 181 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+292 49 moveto (Esyntax) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Printer -> Esyntax
-newpath 284 27 moveto
-293 31 301 36 304 42 curveto
-325 76 321 121 340 156 curveto
-342 160 345 163 350 165 curveto
-stroke
-newpath 348 161 moveto
-356 168 lineto
-346 166 lineto
+newpath 194 137 moveto
+203 133 211 128 216 124 curveto
+232 109 238 86 252 72 curveto
+254 70 256 68 259 66 curveto
+stroke
+newpath 258 64 moveto
+268 61 lineto
+260 68 lineto
closepath
gsave 0 setgray stroke grestore fill
% Esyntax -> Extend
-newpath 404 167 moveto
-419 159 439 149 455 140 curveto
+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
+
+% Prettyp
+gsave 10 dict begin
+48 144 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+48 145 moveto (Prettyp) 40 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Prettyp -> Printer
+newpath 78 145 moveto
+94 146 114 146 131 147 curveto
stroke
-newpath 453 138 moveto
-463 136 lineto
-455 143 lineto
+newpath 130 145 moveto
+140 147 lineto
+130 150 lineto
closepath
gsave 0 setgray stroke grestore fill
% G_zsyntax
gsave 10 dict begin
-136 136 40 18 ellipse_path
+48 86 40 18 ellipse_path
stroke
gsave 10 dict begin
-136 137 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
+48 87 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
end grestore
end grestore
% G_zsyntax -> Astterm
-newpath 162 122 moveto
-180 112 206 99 226 88 curveto
+newpath 88 89 moveto
+101 90 115 91 128 91 curveto
stroke
-newpath 224 86 moveto
-234 84 lineto
-226 91 lineto
+newpath 127 88 moveto
+137 92 lineto
+127 93 lineto
closepath
gsave 0 setgray stroke grestore fill
% G_zsyntax -> Esyntax
-newpath 170 146 moveto
-185 150 201 154 212 156 curveto
-247 163 302 170 340 175 curveto
+newpath 80 75 moveto
+95 71 112 66 124 64 curveto
+159 58 214 54 251 51 curveto
stroke
-newpath 338 172 moveto
-348 176 lineto
-338 177 lineto
+newpath 249 49 moveto
+259 50 lineto
+249 54 lineto
closepath
gsave 0 setgray stroke grestore fill
% G_rsyntax
gsave 10 dict begin
-136 200 39 18 ellipse_path
+48 25 39 18 ellipse_path
stroke
gsave 10 dict begin
-136 201 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
+48 26 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% G_rsyntax -> Astterm
-newpath 157 185 moveto
-164 179 172 172 176 166 curveto
-192 144 195 115 212 96 curveto
-212 96 218 93 225 89 curveto
-stroke
-newpath 224 87 moveto
-234 85 lineto
-226 91 lineto
+newpath 73 39 moveto
+92 50 119 65 139 77 curveto
+stroke
+newpath 139 74 moveto
+147 81 lineto
+137 79 lineto
closepath
gsave 0 setgray stroke grestore fill
% G_rsyntax -> Esyntax
-newpath 175 197 moveto
-220 193 292 187 338 184 curveto
+newpath 88 26 moveto
+126 26 182 28 216 31 curveto
+226 32 242 35 255 38 curveto
stroke
-newpath 337 182 moveto
-347 183 lineto
-337 187 lineto
+newpath 253 35 moveto
+262 40 lineto
+252 40 lineto
closepath
gsave 0 setgray stroke grestore fill
% G_natsyntax
gsave 10 dict begin
-258 126 45 18 ellipse_path
+170 202 45 18 ellipse_path
stroke
gsave 10 dict begin
-258 127 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+170 203 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
end grestore
end grestore
% G_natsyntax -> Termast
-newpath 288 113 moveto
-295 109 300 106 304 102 curveto
-321 85 325 59 340 42 curveto
-343 39 345 37 348 36 curveto
-stroke
-newpath 347 34 moveto
-357 31 lineto
-349 38 lineto
+newpath 203 190 moveto
+219 184 239 176 256 169 curveto
+stroke
+newpath 255 167 moveto
+265 166 lineto
+256 172 lineto
closepath
gsave 0 setgray stroke grestore fill
-% G_natsyntax -> Esyntax
-newpath 288 139 moveto
-306 147 328 157 346 165 curveto
+% G_natsyntax -> Coqlib
+newpath 210 211 moveto
+225 214 241 218 255 221 curveto
stroke
-newpath 346 162 moveto
-355 168 lineto
-345 167 lineto
+newpath 255 218 moveto
+264 223 lineto
+254 223 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Coqlib
-gsave 10 dict begin
-380 126 29 18 ellipse_path
-stroke
-gsave 10 dict begin
-380 127 moveto (Coqlib) 38 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% G_natsyntax -> Coqlib
-newpath 304 126 moveto
-316 126 329 126 340 126 curveto
-stroke
-newpath 340 124 moveto
-350 126 lineto
-340 129 lineto
+% 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
closepath
gsave 0 setgray stroke grestore fill
% Egrammar
gsave 10 dict begin
-380 72 40 18 ellipse_path
+292 102 40 18 ellipse_path
stroke
gsave 10 dict begin
-380 73 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+292 103 moveto (Egrammar) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Egrammar -> Extend
-newpath 407 85 moveto
-421 93 439 101 454 108 curveto
+newpath 320 89 moveto
+334 82 351 74 366 67 curveto
stroke
-newpath 454 105 moveto
-462 112 lineto
-452 110 lineto
+newpath 364 65 moveto
+374 63 lineto
+366 70 lineto
closepath
gsave 0 setgray stroke grestore fill
% Lexer
gsave 10 dict begin
-486 70 27 18 ellipse_path
+398 106 27 18 ellipse_path
stroke
gsave 10 dict begin
-486 71 moveto (Lexer) 32 14.00 -0.50 alignedtext
+398 107 moveto (Lexer) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Egrammar -> Lexer
-newpath 420 71 moveto
-430 71 440 71 449 71 curveto
+newpath 332 104 moveto
+342 104 352 105 361 105 curveto
stroke
-newpath 449 69 moveto
-459 71 lineto
-449 74 lineto
+newpath 361 103 moveto
+371 105 lineto
+361 108 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index c54821490..8af063428 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 576 216
+%%BoundingBox: 36 36 577 203
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,348 +131,550 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 576 216
+%%PageBoundingBox: 36 36 577 203
+%%PageOrientation: Portrait
gsave
-35 35 541 181 boxprim clip newpath
+35 35 542 168 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6444 set_scale
+0.4796 set_scale
0 0 translate 0 rotate
+[ /CropBox [36 36 577 203] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Multcase
gsave 10 dict begin
-347 220 36 18 ellipse_path
+355 234 36 18 ellipse_path
stroke
gsave 10 dict begin
-347 221 moveto (Multcase) 51 14.00 -0.50 alignedtext
+355 235 moveto (Multcase) 51 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarutil
gsave 10 dict begin
-460 220 33 18 ellipse_path
+468 234 33 18 ellipse_path
stroke
gsave 10 dict begin
-460 221 moveto (Evarutil) 45 14.00 -0.50 alignedtext
+468 235 moveto (Evarutil) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Multcase -> Evarutil
-newpath 383 220 moveto
-394 220 406 220 417 220 curveto
+newpath 391 234 moveto
+402 234 414 234 425 234 curveto
stroke
-newpath 417 218 moveto
-427 220 lineto
-417 223 lineto
+newpath 425 232 moveto
+435 234 lineto
+425 237 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pretype_errors
gsave 10 dict begin
-588 261 51 18 ellipse_path
+596 180 51 18 ellipse_path
stroke
gsave 10 dict begin
-588 262 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
+596 181 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarutil -> Pretype_errors
-newpath 489 229 moveto
-504 234 523 240 540 246 curveto
+newpath 494 223 moveto
+511 216 535 206 554 198 curveto
stroke
-newpath 541 244 moveto
-550 249 lineto
-540 249 lineto
+newpath 553 196 moveto
+563 194 lineto
+555 200 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Indrec
+gsave 10 dict begin
+596 288 28 18 ellipse_path
+stroke
+gsave 10 dict begin
+596 289 moveto (Indrec) 35 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Evarutil -> Indrec
+newpath 494 245 moveto
+514 254 542 266 564 275 curveto
+stroke
+newpath 564 272 moveto
+572 278 lineto
+562 277 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Typing
+gsave 10 dict begin
+468 180 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+468 181 moveto (Typing) 40 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Typing -> Pretype_errors
+newpath 499 180 moveto
+510 180 522 180 534 180 curveto
+stroke
+newpath 534 178 moveto
+544 180 lineto
+534 183 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Rawterm
+gsave 10 dict begin
+731 126 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+731 127 moveto (Rawterm) 51 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Pretype_errors -> Rawterm
+newpath 630 166 moveto
+649 158 674 149 694 141 curveto
+stroke
+newpath 692 139 moveto
+702 137 lineto
+694 144 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Inductiveops
+gsave 10 dict begin
+731 180 46 18 ellipse_path
+stroke
+gsave 10 dict begin
+731 181 moveto (Inductiveops) 72 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Pretype_errors -> Inductiveops
+newpath 648 180 moveto
+657 180 665 180 674 180 curveto
+stroke
+newpath 674 178 moveto
+684 180 lineto
+674 183 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacred
gsave 10 dict begin
-712 72 29 18 ellipse_path
+731 34 29 18 ellipse_path
stroke
gsave 10 dict begin
-712 73 moveto (Tacred) 38 14.00 -0.50 alignedtext
+731 35 moveto (Tacred) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Cbv
gsave 10 dict begin
-811 72 27 18 ellipse_path
+863 46 27 18 ellipse_path
stroke
gsave 10 dict begin
-811 73 moveto (Cbv) 23 14.00 -0.50 alignedtext
+863 47 moveto (Cbv) 23 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacred -> Cbv
-newpath 742 72 moveto
-752 72 764 72 774 72 curveto
+newpath 760 37 moveto
+780 39 806 41 827 43 curveto
stroke
-newpath 774 70 moveto
-784 72 lineto
-774 75 lineto
+newpath 826 40 moveto
+836 44 lineto
+826 45 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Syntax_def
+% Reductionops
gsave 10 dict begin
-588 207 42 18 ellipse_path
+863 134 49 18 ellipse_path
stroke
gsave 10 dict begin
-588 208 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
+863 135 moveto (Reductionops) 77 14.00 -0.50 alignedtext
end grestore
end grestore
-% Rawterm
+% Tacred -> Reductionops
+newpath 752 47 moveto
+764 55 778 63 778 63 curveto
+795 75 819 96 837 111 curveto
+stroke
+newpath 838 109 moveto
+844 117 lineto
+835 112 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Instantiate
gsave 10 dict begin
-712 153 36 18 ellipse_path
+988 57 39 18 ellipse_path
stroke
gsave 10 dict begin
-712 154 moveto (Rawterm) 51 14.00 -0.50 alignedtext
+988 58 moveto (Instantiate) 58 14.00 -0.50 alignedtext
end grestore
end grestore
-% Syntax_def -> Rawterm
-newpath 618 194 moveto
-635 186 658 176 676 168 curveto
+% Cbv -> Instantiate
+newpath 890 48 moveto
+904 50 922 51 939 53 curveto
stroke
-newpath 675 166 moveto
-685 165 lineto
-676 171 lineto
+newpath 939 51 moveto
+949 54 lineto
+939 55 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Recordops
+% Reductionops -> Instantiate
+newpath 888 118 moveto
+908 106 936 89 957 77 curveto
+stroke
+newpath 954 76 moveto
+964 72 lineto
+957 80 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Termops
gsave 10 dict begin
-460 126 40 18 ellipse_path
+988 134 35 18 ellipse_path
stroke
gsave 10 dict begin
-460 127 moveto (Recordops) 59 14.00 -0.50 alignedtext
+988 135 moveto (Termops) 49 14.00 -0.50 alignedtext
end grestore
end grestore
-% Classops
+% Reductionops -> Termops
+newpath 912 134 moveto
+923 134 933 134 943 134 curveto
+stroke
+newpath 943 132 moveto
+953 134 lineto
+943 137 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Syntax_def
gsave 10 dict begin
-588 45 35 18 ellipse_path
+596 126 42 18 ellipse_path
stroke
gsave 10 dict begin
-588 46 moveto (Classops) 49 14.00 -0.50 alignedtext
+596 127 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
end grestore
end grestore
-% Recordops -> Classops
-newpath 485 112 moveto
-491 108 496 105 500 102 curveto
-514 93 523 78 536 69 curveto
-541 66 548 63 555 60 curveto
-stroke
-newpath 551 59 moveto
-561 57 lineto
-553 64 lineto
+% Syntax_def -> Rawterm
+newpath 638 126 moveto
+653 126 670 126 685 126 curveto
+stroke
+newpath 685 124 moveto
+695 126 lineto
+685 129 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Classops -> Tacred
-newpath 620 52 moveto
-637 55 657 60 675 64 curveto
+% Retyping
+gsave 10 dict begin
+355 311 36 18 ellipse_path
stroke
-newpath 675 61 moveto
-684 66 lineto
-674 66 lineto
+gsave 10 dict begin
+355 312 moveto (Retyping) 51 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Retyping -> Reductionops
+newpath 388 318 moveto
+450 329 582 348 648 318 curveto
+713 288 802 199 842 157 curveto
+stroke
+newpath 839 157 moveto
+847 151 lineto
+843 160 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Classops -> Rawterm
-newpath 616 56 moveto
-625 60 635 64 640 69 curveto
-656 83 678 109 694 129 curveto
+% Evd
+gsave 10 dict begin
+1091 57 27 18 ellipse_path
stroke
-newpath 695 126 moveto
-699 136 lineto
-691 129 lineto
+gsave 10 dict begin
+1091 58 moveto (Evd) 22 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Instantiate -> Evd
+newpath 1028 57 moveto
+1037 57 1046 57 1054 57 curveto
+stroke
+newpath 1054 55 moveto
+1064 57 lineto
+1054 60 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Retyping
+% Recordops
+gsave 10 dict begin
+468 72 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+468 73 moveto (Recordops) 59 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Classops
gsave 10 dict begin
-712 18 36 18 ellipse_path
+596 18 35 18 ellipse_path
stroke
gsave 10 dict begin
-712 19 moveto (Retyping) 51 14.00 -0.50 alignedtext
+596 19 moveto (Classops) 49 14.00 -0.50 alignedtext
end grestore
end grestore
-% Classops -> Retyping
-newpath 620 38 moveto
-635 35 653 31 669 27 curveto
+% Recordops -> Classops
+newpath 497 60 moveto
+516 52 541 41 561 33 curveto
+stroke
+newpath 559 31 moveto
+569 30 lineto
+561 36 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Classops -> Tacred
+newpath 630 22 moveto
+649 25 673 27 693 30 curveto
stroke
-newpath 669 25 moveto
-679 25 lineto
-670 29 lineto
+newpath 692 27 moveto
+702 31 lineto
+692 32 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Classops -> Rawterm
+newpath 622 30 moveto
+635 36 648 42 648 42 curveto
+667 56 692 83 710 103 curveto
+stroke
+newpath 711 100 moveto
+716 109 lineto
+707 104 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pretyping
gsave 10 dict begin
-38 126 37 18 ellipse_path
+46 245 37 18 ellipse_path
stroke
gsave 10 dict begin
-38 127 moveto (Pretyping) 54 14.00 -0.50 alignedtext
+46 246 moveto (Pretyping) 54 14.00 -0.50 alignedtext
end grestore
end grestore
% Cases
gsave 10 dict begin
-139 126 27 18 ellipse_path
+147 245 27 18 ellipse_path
stroke
gsave 10 dict begin
-139 127 moveto (Cases) 32 14.00 -0.50 alignedtext
+147 246 moveto (Cases) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Pretyping -> Cases
-newpath 76 126 moveto
-85 126 94 126 102 126 curveto
+newpath 84 245 moveto
+93 245 102 245 110 245 curveto
stroke
-newpath 102 124 moveto
-112 126 lineto
-102 129 lineto
+newpath 110 243 moveto
+120 245 lineto
+110 248 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coercion
gsave 10 dict begin
-238 126 36 18 ellipse_path
+246 245 36 18 ellipse_path
stroke
gsave 10 dict begin
-238 127 moveto (Coercion) 51 14.00 -0.50 alignedtext
+246 246 moveto (Coercion) 51 14.00 -0.50 alignedtext
end grestore
end grestore
% Cases -> Coercion
-newpath 166 126 moveto
-174 126 183 126 192 126 curveto
+newpath 174 245 moveto
+182 245 191 245 200 245 curveto
stroke
-newpath 192 124 moveto
-202 126 lineto
-192 129 lineto
+newpath 200 243 moveto
+210 245 lineto
+200 248 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Pretype_errors -> Rawterm
-newpath 623 248 moveto
-629 244 636 241 640 237 curveto
-656 223 678 197 694 177 curveto
+% Inductiveops -> Reductionops
+newpath 766 168 moveto
+782 162 801 155 818 149 curveto
stroke
-newpath 691 177 moveto
-699 170 lineto
-695 180 lineto
+newpath 817 147 moveto
+827 146 lineto
+818 152 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pattern
gsave 10 dict begin
-588 153 30 18 ellipse_path
+596 72 30 18 ellipse_path
stroke
gsave 10 dict begin
-588 154 moveto (Pattern) 39 14.00 -0.50 alignedtext
+596 73 moveto (Pattern) 39 14.00 -0.50 alignedtext
end grestore
end grestore
+% Pattern -> Reductionops
+newpath 626 75 moveto
+666 79 737 86 778 96 curveto
+785 98 806 107 826 117 curveto
+stroke
+newpath 825 114 moveto
+833 120 lineto
+823 118 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% Pattern -> Rawterm
-newpath 618 153 moveto
-632 153 650 153 666 153 curveto
+newpath 621 82 moveto
+641 91 671 102 694 112 curveto
+stroke
+newpath 694 109 moveto
+703 115 lineto
+693 114 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Indrec -> Inductiveops
+newpath 620 279 moveto
+631 274 642 269 648 264 curveto
+666 250 692 223 710 204 curveto
stroke
-newpath 666 151 moveto
-676 153 lineto
-666 156 lineto
+newpath 708 203 moveto
+716 197 lineto
+711 206 lineto
closepath
gsave 0 setgray stroke grestore fill
% Evarconv
gsave 10 dict begin
-347 126 37 18 ellipse_path
+355 180 37 18 ellipse_path
stroke
gsave 10 dict begin
-347 127 moveto (Evarconv) 53 14.00 -0.50 alignedtext
+355 181 moveto (Evarconv) 53 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarconv -> Evarutil
-newpath 366 142 moveto
-385 157 414 181 435 199 curveto
+newpath 381 193 moveto
+397 201 418 211 435 218 curveto
stroke
-newpath 436 197 moveto
-442 205 lineto
-433 200 lineto
+newpath 435 215 moveto
+443 222 lineto
+433 220 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Evarconv -> Recordops
-newpath 384 126 moveto
-392 126 401 126 410 126 curveto
+% Evarconv -> Typing
+newpath 392 180 moveto
+404 180 416 180 427 180 curveto
stroke
-newpath 410 124 moveto
-420 126 lineto
-410 129 lineto
+newpath 427 178 moveto
+437 180 lineto
+427 183 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Typing
-gsave 10 dict begin
-460 72 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-460 73 moveto (Typing) 40 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Evarconv -> Typing
-newpath 373 113 moveto
-389 105 411 95 428 87 curveto
+% Evarconv -> Recordops
+newpath 372 164 moveto
+391 145 422 116 444 95 curveto
stroke
-newpath 426 85 moveto
-436 83 lineto
-428 90 lineto
+newpath 442 93 moveto
+451 88 lineto
+446 97 lineto
closepath
gsave 0 setgray stroke grestore fill
% Detyping
gsave 10 dict begin
-588 99 36 18 ellipse_path
+596 234 36 18 ellipse_path
stroke
gsave 10 dict begin
-588 100 moveto (Detyping) 52 14.00 -0.50 alignedtext
+596 235 moveto (Detyping) 52 14.00 -0.50 alignedtext
end grestore
end grestore
% Detyping -> Rawterm
-newpath 616 111 moveto
-633 119 657 129 676 137 curveto
+newpath 626 223 moveto
+634 220 643 215 648 210 curveto
+665 193 668 166 684 150 curveto
+684 150 689 147 697 144 curveto
+stroke
+newpath 696 142 moveto
+706 139 lineto
+698 146 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Detyping -> Termops
+newpath 632 230 moveto
+673 226 739 219 778 210 curveto
+825 199 868 180 912 164 curveto
+912 164 932 156 951 149 curveto
+stroke
+newpath 950 147 moveto
+960 145 lineto
+952 151 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Coercion -> Retyping
+newpath 269 259 moveto
+285 269 306 282 324 292 curveto
stroke
-newpath 677 135 moveto
-685 141 lineto
-675 139 lineto
+newpath 325 290 moveto
+332 297 lineto
+322 294 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coercion -> Evarconv
-newpath 274 126 moveto
-282 126 291 126 300 126 curveto
+newpath 269 231 moveto
+285 222 306 209 323 199 curveto
stroke
-newpath 300 124 moveto
-310 126 lineto
-300 129 lineto
+newpath 321 197 moveto
+331 194 lineto
+324 201 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index d5d247a2c..28297b5aa 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 125
+%%BoundingBox: 36 36 577 124
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,211 +131,224 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 125
+%%PageBoundingBox: 36 36 577 124
+%%PageOrientation: Portrait
gsave
-35 35 542 90 boxprim clip newpath
+35 35 542 89 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6178 set_scale
+0.6067 set_scale
0 0 translate 0 rotate
+[ /CropBox [36 36 577 124] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Tactic_debug
gsave 10 dict begin
-159 126 48 18 ellipse_path
+167 126 48 18 ellipse_path
stroke
gsave 10 dict begin
-159 127 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
+167 127 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacmach
gsave 10 dict begin
-280 72 36 18 ellipse_path
+288 72 36 18 ellipse_path
stroke
gsave 10 dict begin
-280 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
+288 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
end grestore
end grestore
% Tactic_debug -> Tacmach
-newpath 190 112 moveto
-207 104 227 95 244 88 curveto
+newpath 198 112 moveto
+215 104 235 95 252 88 curveto
stroke
-newpath 243 86 moveto
-253 84 lineto
-245 90 lineto
+newpath 251 86 moveto
+261 84 lineto
+253 90 lineto
closepath
gsave 0 setgray stroke grestore fill
% Evar_refiner
gsave 10 dict begin
-398 72 45 18 ellipse_path
+406 72 45 18 ellipse_path
stroke
gsave 10 dict begin
-398 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
+406 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacmach -> Evar_refiner
-newpath 316 72 moveto
-324 72 333 72 342 72 curveto
+newpath 324 72 moveto
+332 72 341 72 350 72 curveto
stroke
-newpath 342 70 moveto
-352 72 lineto
-342 75 lineto
+newpath 350 70 moveto
+360 72 lineto
+350 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Refiner
gsave 10 dict begin
-511 72 31 18 ellipse_path
+519 72 31 18 ellipse_path
stroke
gsave 10 dict begin
-511 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
+519 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
end grestore
end grestore
% Evar_refiner -> Refiner
-newpath 444 72 moveto
-453 72 462 72 470 72 curveto
+newpath 452 72 moveto
+461 72 470 72 478 72 curveto
stroke
-newpath 470 70 moveto
-480 72 lineto
-470 75 lineto
+newpath 478 70 moveto
+488 72 lineto
+478 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacinterp
gsave 10 dict begin
-37 99 37 18 ellipse_path
+45 99 37 18 ellipse_path
stroke
gsave 10 dict begin
-37 100 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
+45 100 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacinterp -> Tactic_debug
-newpath 71 107 moveto
-82 109 95 112 107 115 curveto
+newpath 79 107 moveto
+90 109 103 112 115 115 curveto
stroke
-newpath 108 113 moveto
-117 117 lineto
-107 117 lineto
+newpath 116 113 moveto
+125 117 lineto
+115 117 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pfedit
gsave 10 dict begin
-159 72 27 18 ellipse_path
+167 72 27 18 ellipse_path
stroke
gsave 10 dict begin
-159 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
+167 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacinterp -> Pfedit
-newpath 71 91 moveto
-88 88 108 83 124 80 curveto
+newpath 79 91 moveto
+96 88 116 83 132 80 curveto
stroke
-newpath 123 78 moveto
-133 78 lineto
-124 83 lineto
+newpath 131 78 moveto
+141 78 lineto
+132 83 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pfedit -> Tacmach
-newpath 186 72 moveto
-200 72 218 72 234 72 curveto
+newpath 194 72 moveto
+208 72 226 72 242 72 curveto
stroke
-newpath 234 70 moveto
-244 72 lineto
-234 75 lineto
+newpath 242 70 moveto
+252 72 lineto
+242 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Logic
gsave 10 dict begin
-605 72 27 18 ellipse_path
+613 72 27 18 ellipse_path
stroke
gsave 10 dict begin
-605 73 moveto (Logic) 32 14.00 -0.50 alignedtext
+613 73 moveto (Logic) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Refiner -> Logic
-newpath 542 72 moveto
-550 72 559 72 568 72 curveto
+newpath 550 72 moveto
+558 72 567 72 576 72 curveto
stroke
-newpath 568 70 moveto
-578 72 lineto
-568 75 lineto
+newpath 576 70 moveto
+586 72 lineto
+576 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Proof_trees
gsave 10 dict begin
-711 72 42 18 ellipse_path
+719 72 42 18 ellipse_path
stroke
gsave 10 dict begin
-711 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
+719 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
end grestore
end grestore
% Logic -> Proof_trees
-newpath 632 72 moveto
-640 72 649 72 658 72 curveto
+newpath 640 72 moveto
+648 72 657 72 666 72 curveto
stroke
-newpath 658 70 moveto
-668 72 lineto
-658 75 lineto
+newpath 666 70 moveto
+676 72 lineto
+666 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Proof_type
gsave 10 dict begin
-832 72 41 18 ellipse_path
+840 72 41 18 ellipse_path
stroke
gsave 10 dict begin
-832 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
+840 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
end grestore
end grestore
% Proof_trees -> Proof_type
-newpath 754 72 moveto
-763 72 772 72 780 72 curveto
+newpath 762 72 moveto
+771 72 780 72 788 72 curveto
stroke
-newpath 780 70 moveto
-790 72 lineto
-780 75 lineto
+newpath 788 70 moveto
+798 72 lineto
+788 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Clenv
gsave 10 dict begin
-159 18 27 18 ellipse_path
+167 18 27 18 ellipse_path
stroke
gsave 10 dict begin
-159 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
+167 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
end grestore
end grestore
% Clenv -> Tacmach
-newpath 181 28 moveto
-198 36 224 48 244 56 curveto
+newpath 189 28 moveto
+206 36 232 48 252 56 curveto
stroke
-newpath 245 54 moveto
-253 60 lineto
-243 58 lineto
+newpath 253 54 moveto
+261 60 lineto
+251 58 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 5e8125d5e..a628a56d9 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 193
+%%BoundingBox: 36 36 577 125
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,435 +131,444 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 193
+%%PageBoundingBox: 36 36 577 125
+%%PageOrientation: Portrait
gsave
-35 35 542 158 boxprim clip newpath
+35 35 542 90 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6250 set_scale
+0.4865 set_scale
0 0 translate 0 rotate
+[ /CropBox [36 36 577 125] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Termdn
gsave 10 dict begin
-701 233 32 18 ellipse_path
+939 18 32 18 ellipse_path
stroke
gsave 10 dict begin
-701 234 moveto (Termdn) 44 14.00 -0.50 alignedtext
+939 19 moveto (Termdn) 44 14.00 -0.50 alignedtext
end grestore
end grestore
% Dn
gsave 10 dict begin
-819 233 27 18 ellipse_path
+1057 18 27 18 ellipse_path
stroke
gsave 10 dict begin
-819 234 moveto (Dn) 17 14.00 -0.50 alignedtext
+1057 19 moveto (Dn) 17 14.00 -0.50 alignedtext
end grestore
end grestore
% Termdn -> Dn
-newpath 734 233 moveto
-749 233 767 233 783 233 curveto
+newpath 972 18 moveto
+987 18 1005 18 1021 18 curveto
stroke
-newpath 782 231 moveto
-792 233 lineto
-782 236 lineto
+newpath 1020 16 moveto
+1030 18 lineto
+1020 21 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tactics
gsave 10 dict begin
-593 110 30 18 ellipse_path
+831 118 30 18 ellipse_path
stroke
gsave 10 dict begin
-593 111 moveto (Tactics) 40 14.00 -0.50 alignedtext
+831 119 moveto (Tactics) 40 14.00 -0.50 alignedtext
end grestore
end grestore
% Hipattern
gsave 10 dict begin
-701 156 36 18 ellipse_path
+939 149 36 18 ellipse_path
stroke
gsave 10 dict begin
-701 157 moveto (Hipattern) 52 14.00 -0.50 alignedtext
+939 150 moveto (Hipattern) 52 14.00 -0.50 alignedtext
end grestore
end grestore
% Tactics -> Hipattern
-newpath 618 121 moveto
-631 127 649 134 664 140 curveto
+newpath 859 126 moveto
+871 129 885 133 898 137 curveto
stroke
-newpath 665 138 moveto
-673 144 lineto
-663 142 lineto
+newpath 898 134 moveto
+907 140 lineto
+897 139 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacticals
gsave 10 dict begin
-701 102 35 18 ellipse_path
+939 95 35 18 ellipse_path
stroke
gsave 10 dict begin
-701 103 moveto (Tacticals) 50 14.00 -0.50 alignedtext
+939 96 moveto (Tacticals) 50 14.00 -0.50 alignedtext
end grestore
end grestore
% Tactics -> Tacticals
-newpath 623 108 moveto
-633 107 645 106 656 105 curveto
+newpath 860 112 moveto
+871 110 884 107 896 104 curveto
stroke
-newpath 656 103 moveto
-666 104 lineto
-656 107 lineto
+newpath 896 102 moveto
+906 102 lineto
+897 106 lineto
closepath
gsave 0 setgray stroke grestore fill
% Wcclausenv
gsave 10 dict begin
-819 102 44 18 ellipse_path
+1057 95 44 18 ellipse_path
stroke
gsave 10 dict begin
-819 103 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
+1057 96 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacticals -> Wcclausenv
-newpath 737 102 moveto
-746 102 755 102 764 102 curveto
+newpath 975 95 moveto
+984 95 993 95 1002 95 curveto
stroke
-newpath 764 100 moveto
-774 102 lineto
-764 105 lineto
+newpath 1002 93 moveto
+1012 95 lineto
+1002 98 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacentries
gsave 10 dict begin
-482 141 39 18 ellipse_path
+720 164 39 18 ellipse_path
stroke
gsave 10 dict begin
-482 142 moveto (Tacentries) 58 14.00 -0.50 alignedtext
+720 165 moveto (Tacentries) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacentries -> Tactics
-newpath 516 132 moveto
-529 128 543 124 556 120 curveto
+newpath 749 152 moveto
+764 146 782 138 797 132 curveto
stroke
-newpath 555 118 moveto
-565 118 lineto
-556 123 lineto
+newpath 796 130 moveto
+806 128 lineto
+798 134 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Refine
+% Setoid_replace
gsave 10 dict begin
-482 87 29 18 ellipse_path
+388 110 52 18 ellipse_path
stroke
gsave 10 dict begin
-482 88 moveto (Refine) 37 14.00 -0.50 alignedtext
+388 111 moveto (Setoid_replace) 83 14.00 -0.50 alignedtext
end grestore
end grestore
-% Refine -> Tactics
-newpath 510 93 moveto
-523 95 540 99 554 102 curveto
+% Auto
+gsave 10 dict begin
+503 110 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+503 111 moveto (Auto) 28 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Setoid_replace -> Auto
+newpath 440 110 moveto
+449 110 458 110 466 110 curveto
stroke
-newpath 555 100 moveto
-564 104 lineto
-554 104 lineto
+newpath 466 108 moveto
+476 110 lineto
+466 113 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Nbtermdn
+% Hiddentac
gsave 10 dict begin
-482 233 38 18 ellipse_path
+605 164 39 18 ellipse_path
stroke
gsave 10 dict begin
-482 234 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
+605 165 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
end grestore
end grestore
-% Btermdn
+% Auto -> Hiddentac
+newpath 525 121 moveto
+538 129 556 138 571 146 curveto
+stroke
+newpath 572 144 moveto
+580 150 lineto
+570 148 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Dhyp
gsave 10 dict begin
-593 233 35 18 ellipse_path
+605 110 27 18 ellipse_path
stroke
gsave 10 dict begin
-593 234 moveto (Btermdn) 49 14.00 -0.50 alignedtext
+605 111 moveto (Dhyp) 31 14.00 -0.50 alignedtext
end grestore
end grestore
-% Nbtermdn -> Btermdn
-newpath 521 233 moveto
-530 233 539 233 548 233 curveto
+% Auto -> Dhyp
+newpath 530 110 moveto
+542 110 556 110 568 110 curveto
stroke
-newpath 548 231 moveto
-558 233 lineto
-548 236 lineto
+newpath 568 108 moveto
+578 110 lineto
+568 113 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Btermdn -> Termdn
-newpath 628 233 moveto
-638 233 649 233 659 233 curveto
+% Refine
+gsave 10 dict begin
+720 72 29 18 ellipse_path
stroke
-newpath 658 231 moveto
-668 233 lineto
-658 236 lineto
+gsave 10 dict begin
+720 73 moveto (Refine) 37 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Refine -> Tactics
+newpath 744 82 moveto
+759 89 780 97 797 104 curveto
+stroke
+newpath 798 102 moveto
+806 108 lineto
+796 106 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Leminv
+% Nbtermdn
gsave 10 dict begin
-32 126 32 18 ellipse_path
+720 18 38 18 ellipse_path
stroke
gsave 10 dict begin
-32 127 moveto (Leminv) 43 14.00 -0.50 alignedtext
+720 19 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
end grestore
end grestore
-% Inv
+% Btermdn
gsave 10 dict begin
-144 126 27 18 ellipse_path
+831 18 35 18 ellipse_path
stroke
gsave 10 dict begin
-144 127 moveto (Inv) 18 14.00 -0.50 alignedtext
+831 19 moveto (Btermdn) 49 14.00 -0.50 alignedtext
end grestore
end grestore
-% Leminv -> Inv
-newpath 64 126 moveto
-78 126 94 126 108 126 curveto
+% Nbtermdn -> Btermdn
+newpath 759 18 moveto
+768 18 777 18 786 18 curveto
stroke
-newpath 107 124 moveto
-117 126 lineto
-107 129 lineto
+newpath 786 16 moveto
+796 18 lineto
+786 21 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Auto
-gsave 10 dict begin
-258 180 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-258 181 moveto (Auto) 28 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Inv -> Auto
-newpath 166 137 moveto
-183 145 208 156 227 165 curveto
+% Btermdn -> Termdn
+newpath 866 18 moveto
+876 18 887 18 897 18 curveto
stroke
-newpath 228 163 moveto
-236 169 lineto
-226 167 lineto
+newpath 896 16 moveto
+906 18 lineto
+896 21 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Elim
+% Leminv
gsave 10 dict begin
-258 126 27 18 ellipse_path
+40 164 32 18 ellipse_path
stroke
gsave 10 dict begin
-258 127 moveto (Elim) 27 14.00 -0.50 alignedtext
+40 165 moveto (Leminv) 43 14.00 -0.50 alignedtext
end grestore
end grestore
-% Inv -> Elim
-newpath 171 126 moveto
-186 126 205 126 222 126 curveto
-stroke
-newpath 221 124 moveto
-231 126 lineto
-221 129 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Equality
+% Inv
gsave 10 dict begin
-258 62 34 18 ellipse_path
+152 164 27 18 ellipse_path
stroke
gsave 10 dict begin
-258 63 moveto (Equality) 47 14.00 -0.50 alignedtext
+152 165 moveto (Inv) 18 14.00 -0.50 alignedtext
end grestore
end grestore
-% Inv -> Equality
-newpath 165 114 moveto
-183 104 207 91 227 80 curveto
+% Leminv -> Inv
+newpath 72 164 moveto
+86 164 102 164 116 164 curveto
stroke
-newpath 225 78 moveto
-235 75 lineto
-228 82 lineto
+newpath 115 162 moveto
+125 164 lineto
+115 167 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Hiddentac
+% Elim
gsave 10 dict begin
-367 137 39 18 ellipse_path
+503 164 27 18 ellipse_path
stroke
gsave 10 dict begin
-367 138 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
+503 165 moveto (Elim) 27 14.00 -0.50 alignedtext
end grestore
end grestore
-% Auto -> Hiddentac
-newpath 281 171 moveto
-294 165 313 159 328 153 curveto
+% Inv -> Elim
+newpath 179 164 moveto
+242 164 396 164 467 164 curveto
stroke
-newpath 327 151 moveto
-337 149 lineto
-329 155 lineto
+newpath 466 162 moveto
+476 164 lineto
+466 167 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Dhyp
+% Equality
gsave 10 dict begin
-367 191 27 18 ellipse_path
+266 110 34 18 ellipse_path
stroke
gsave 10 dict begin
-367 192 moveto (Dhyp) 31 14.00 -0.50 alignedtext
+266 111 moveto (Equality) 47 14.00 -0.50 alignedtext
end grestore
end grestore
-% Auto -> Dhyp
-newpath 285 183 moveto
-299 185 316 186 330 187 curveto
+% Inv -> Equality
+newpath 174 153 moveto
+190 145 213 134 231 126 curveto
stroke
-newpath 330 185 moveto
-340 188 lineto
-330 189 lineto
+newpath 230 124 moveto
+240 122 lineto
+232 128 lineto
closepath
gsave 0 setgray stroke grestore fill
% Elim -> Hiddentac
-newpath 285 129 moveto
-295 130 307 131 319 132 curveto
+newpath 530 164 moveto
+538 164 547 164 556 164 curveto
stroke
-newpath 319 130 moveto
-329 133 lineto
-319 134 lineto
+newpath 556 162 moveto
+566 164 lineto
+556 167 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Equality -> Tactics
-newpath 291 57 moveto
-347 48 461 36 522 57 curveto
-536 62 555 76 569 89 curveto
+% Equality -> Setoid_replace
+newpath 300 110 moveto
+308 110 317 110 326 110 curveto
stroke
-newpath 570 87 moveto
-576 95 lineto
-567 90 lineto
+newpath 326 108 moveto
+336 110 lineto
+326 113 lineto
closepath
gsave 0 setgray stroke grestore fill
% Hiddentac -> Tacentries
-newpath 406 138 moveto
-415 139 423 139 432 139 curveto
+newpath 644 164 moveto
+653 164 662 164 670 164 curveto
stroke
-newpath 432 137 moveto
-442 140 lineto
-432 141 lineto
+newpath 670 162 moveto
+680 164 lineto
+670 167 lineto
closepath
gsave 0 setgray stroke grestore fill
% Eqdecide
gsave 10 dict begin
-144 72 36 18 ellipse_path
+152 110 36 18 ellipse_path
stroke
gsave 10 dict begin
-144 73 moveto (Eqdecide) 51 14.00 -0.50 alignedtext
+152 111 moveto (Eqdecide) 51 14.00 -0.50 alignedtext
end grestore
end grestore
-% Eqdecide -> Auto
-newpath 171 84 moveto
-178 88 184 92 188 96 curveto
-205 113 210 139 224 156 curveto
-225 158 227 160 229 162 curveto
-stroke
-newpath 231 160 moveto
-238 168 lineto
-228 165 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
% Eqdecide -> Equality
-newpath 180 69 moveto
-191 68 203 67 214 66 curveto
+newpath 189 110 moveto
+200 110 211 110 222 110 curveto
stroke
-newpath 214 64 moveto
-224 65 lineto
-214 68 lineto
+newpath 222 108 moveto
+232 110 lineto
+222 113 lineto
closepath
gsave 0 setgray stroke grestore fill
% Eauto
gsave 10 dict begin
-144 180 27 18 ellipse_path
+388 56 27 18 ellipse_path
stroke
gsave 10 dict begin
-144 181 moveto (Eauto) 32 14.00 -0.50 alignedtext
+388 57 moveto (Eauto) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Eauto -> Auto
-newpath 171 180 moveto
-186 180 205 180 222 180 curveto
+newpath 410 66 moveto
+428 75 453 86 473 95 curveto
stroke
-newpath 221 178 moveto
-231 180 lineto
-221 183 lineto
+newpath 473 92 moveto
+481 99 lineto
+471 97 lineto
closepath
gsave 0 setgray stroke grestore fill
% Dhyp -> Tactics
-newpath 394 190 moveto
-429 188 489 183 522 171 curveto
-538 166 558 148 573 133 curveto
+newpath 632 111 moveto
+671 112 745 115 791 117 curveto
stroke
-newpath 571 132 moveto
-579 126 lineto
-574 135 lineto
+newpath 790 115 moveto
+800 117 lineto
+790 120 lineto
closepath
gsave 0 setgray stroke grestore fill
% Dhyp -> Nbtermdn
-newpath 391 200 moveto
-406 205 426 212 442 219 curveto
+newpath 621 95 moveto
+638 80 663 56 680 42 curveto
+682 41 684 39 686 38 curveto
stroke
-newpath 442 216 moveto
-451 222 lineto
-441 221 lineto
+newpath 685 35 moveto
+695 32 lineto
+688 40 lineto
closepath
gsave 0 setgray stroke grestore fill
% Autorewrite
gsave 10 dict begin
-144 18 44 18 ellipse_path
+152 56 44 18 ellipse_path
stroke
gsave 10 dict begin
-144 19 moveto (Autorewrite) 67 14.00 -0.50 alignedtext
+152 57 moveto (Autorewrite) 67 14.00 -0.50 alignedtext
end grestore
end grestore
% Autorewrite -> Equality
-newpath 176 30 moveto
-190 36 207 42 222 48 curveto
+newpath 181 70 moveto
+196 78 216 87 232 94 curveto
stroke
-newpath 222 45 moveto
-231 51 lineto
-221 50 lineto
+newpath 233 92 moveto
+241 98 lineto
+231 96 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index ef9c5f163..725910c85 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
-%%Creator: dot version uwin98 (01-26-98)
-%%For: Gros nain
+%%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
+%%For: (herbelin) Hugo Herbelin
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 576 260
+%%BoundingBox: 36 36 576 256
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (() show i str cvs show (,) show j str cvs show ()) show
+ (\() show i str cvs show (,) show j str cvs show (\)) show
grestore
} if
} bind def
@@ -131,436 +131,449 @@ def
/curlayer 0 def
-%%EndResource
%%EndProlog
%%BeginSetup
14 default-font-family set_font
+1 setmiterlimit
% /arrowlength 10 def
% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+ userdict (<<) cvn ([) cvn load put
+ userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndResource
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 576 260
+%%PageBoundingBox: 36 36 576 256
+%%PageOrientation: Portrait
gsave
-35 35 541 225 boxprim clip newpath
+35 35 541 221 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6353 set_scale
+0.6236 set_scale
0 0 translate 0 rotate
+[ /CropBox [36 36 576 256] /PAGES pdfmark
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
+% Vernac
+gsave 10 dict begin
+542 226 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+542 227 moveto (Vernac) 40 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
% Vernacinterp
gsave 10 dict begin
-687 234 46 18 ellipse_path
+695 234 46 18 ellipse_path
stroke
gsave 10 dict begin
-687 235 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
+695 235 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
end grestore
end grestore
+% Vernac -> Vernacinterp
+newpath 573 228 moveto
+592 229 619 230 642 231 curveto
+stroke
+newpath 639 228 moveto
+649 232 lineto
+639 233 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% Command
gsave 10 dict begin
-810 203 39 18 ellipse_path
+818 203 39 18 ellipse_path
stroke
gsave 10 dict begin
-810 204 moveto (Command) 58 14.00 -0.50 alignedtext
+818 204 moveto (Command) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacinterp -> Command
-newpath 726 224 moveto
-739 221 753 218 766 214 curveto
+newpath 734 224 moveto
+747 221 761 218 774 214 curveto
stroke
-newpath 765 212 moveto
-775 212 lineto
-766 217 lineto
+newpath 773 212 moveto
+783 212 lineto
+774 217 lineto
closepath
gsave 0 setgray stroke grestore fill
% Himsg
gsave 10 dict begin
-810 257 29 18 ellipse_path
+818 257 29 18 ellipse_path
stroke
gsave 10 dict begin
-810 258 moveto (Himsg) 37 14.00 -0.50 alignedtext
+818 258 moveto (Himsg) 37 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacinterp -> Himsg
-newpath 729 242 moveto
-744 244 759 248 773 250 curveto
+newpath 737 242 moveto
+752 244 767 248 781 250 curveto
stroke
-newpath 773 247 moveto
-782 252 lineto
-772 252 lineto
+newpath 781 247 moveto
+790 252 lineto
+780 252 lineto
closepath
gsave 0 setgray stroke grestore fill
% Vernacentries
gsave 10 dict begin
-534 126 49 18 ellipse_path
+542 126 49 18 ellipse_path
stroke
gsave 10 dict begin
-534 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
+542 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacentries -> Vernacinterp
-newpath 554 143 moveto
-578 162 616 193 640 210 curveto
-643 212 647 215 652 217 curveto
+newpath 562 143 moveto
+586 162 624 193 648 210 curveto
+651 212 655 215 660 217 curveto
stroke
-newpath 650 213 moveto
-658 220 lineto
-648 218 lineto
+newpath 658 213 moveto
+666 220 lineto
+656 218 lineto
closepath
gsave 0 setgray stroke grestore fill
% Discharge
gsave 10 dict begin
-687 126 38 18 ellipse_path
+695 126 38 18 ellipse_path
stroke
gsave 10 dict begin
-687 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
+695 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacentries -> Discharge
-newpath 583 126 moveto
-601 126 621 126 639 126 curveto
+newpath 591 126 moveto
+609 126 629 126 647 126 curveto
stroke
-newpath 638 124 moveto
-648 126 lineto
-638 129 lineto
+newpath 646 124 moveto
+656 126 lineto
+646 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Metasyntax
gsave 10 dict begin
-687 72 43 18 ellipse_path
+695 72 43 18 ellipse_path
stroke
gsave 10 dict begin
-687 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
+695 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacentries -> Metasyntax
-newpath 569 113 moveto
-592 106 622 96 645 87 curveto
+newpath 577 113 moveto
+600 106 630 96 653 87 curveto
stroke
-newpath 644 85 moveto
-654 84 lineto
-645 90 lineto
+newpath 652 85 moveto
+662 84 lineto
+653 90 lineto
closepath
gsave 0 setgray stroke grestore fill
% Mltop
gsave 10 dict begin
-687 18 27 18 ellipse_path
+695 18 27 18 ellipse_path
stroke
gsave 10 dict begin
-687 19 moveto (Mltop) 34 14.00 -0.50 alignedtext
+695 19 moveto (Mltop) 34 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacentries -> Mltop
-newpath 554 109 moveto
-578 90 616 59 640 42 curveto
-645 39 651 35 658 32 curveto
+newpath 562 109 moveto
+586 90 624 59 648 42 curveto
+653 39 659 35 666 32 curveto
stroke
-newpath 654 31 moveto
-664 29 lineto
-656 36 lineto
+newpath 662 31 moveto
+672 29 lineto
+664 36 lineto
closepath
gsave 0 setgray stroke grestore fill
% Record
gsave 10 dict begin
-687 180 30 18 ellipse_path
+695 180 30 18 ellipse_path
stroke
gsave 10 dict begin
-687 181 moveto (Record) 40 14.00 -0.50 alignedtext
+695 181 moveto (Record) 40 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacentries -> Record
-newpath 569 139 moveto
-594 147 628 159 653 168 curveto
+newpath 577 139 moveto
+602 147 636 159 661 168 curveto
stroke
-newpath 653 165 moveto
-661 171 lineto
-651 170 lineto
+newpath 661 165 moveto
+669 171 lineto
+659 170 lineto
closepath
gsave 0 setgray stroke grestore fill
% Class
gsave 10 dict begin
-810 149 27 18 ellipse_path
+818 149 27 18 ellipse_path
stroke
gsave 10 dict begin
-810 150 moveto (Class) 30 14.00 -0.50 alignedtext
+818 150 moveto (Class) 30 14.00 -0.50 alignedtext
end grestore
end grestore
% Discharge -> Class
-newpath 723 133 moveto
-739 136 758 140 775 142 curveto
+newpath 731 133 moveto
+747 136 766 140 783 142 curveto
stroke
-newpath 775 139 moveto
-784 144 lineto
-774 144 lineto
+newpath 783 139 moveto
+792 144 lineto
+782 144 lineto
closepath
gsave 0 setgray stroke grestore fill
% Recordobj
gsave 10 dict begin
-810 95 39 18 ellipse_path
+818 95 39 18 ellipse_path
stroke
gsave 10 dict begin
-810 96 moveto (Recordobj) 58 14.00 -0.50 alignedtext
+818 96 moveto (Recordobj) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Discharge -> Recordobj
-newpath 721 117 moveto
-735 114 751 110 766 106 curveto
+newpath 729 117 moveto
+743 114 759 110 774 106 curveto
stroke
-newpath 765 104 moveto
-775 104 lineto
-766 109 lineto
+newpath 773 104 moveto
+783 104 lineto
+774 109 lineto
closepath
gsave 0 setgray stroke grestore fill
% Record -> Command
-newpath 716 185 moveto
-730 187 748 191 763 194 curveto
+newpath 724 185 moveto
+738 187 756 191 771 194 curveto
stroke
-newpath 764 192 moveto
-773 196 lineto
-763 196 lineto
+newpath 772 192 moveto
+781 196 lineto
+771 196 lineto
closepath
gsave 0 setgray stroke grestore fill
% Record -> Himsg
-newpath 710 192 moveto
-722 198 734 204 734 204 curveto
-747 212 758 224 770 233 curveto
-773 235 778 238 783 240 curveto
-stroke
-newpath 782 236 moveto
-789 244 lineto
-779 241 lineto
+newpath 718 192 moveto
+730 198 742 204 742 204 curveto
+755 212 766 224 778 233 curveto
+781 235 786 238 791 240 curveto
+stroke
+newpath 790 236 moveto
+797 244 lineto
+787 241 lineto
closepath
gsave 0 setgray stroke grestore fill
% Record -> Class
-newpath 715 173 moveto
-733 169 756 163 776 158 curveto
-stroke
-newpath 775 156 moveto
-785 156 lineto
-776 161 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Vernac
-gsave 10 dict begin
-534 226 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-534 227 moveto (Vernac) 40 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Vernac -> Vernacinterp
-newpath 565 228 moveto
-584 229 611 230 634 231 curveto
+newpath 723 173 moveto
+741 169 764 163 784 158 curveto
stroke
-newpath 631 228 moveto
-641 232 lineto
-631 233 lineto
+newpath 783 156 moveto
+793 156 lineto
+784 161 lineto
closepath
gsave 0 setgray stroke grestore fill
% Toplevel
gsave 10 dict begin
-239 122 35 18 ellipse_path
+247 122 35 18 ellipse_path
stroke
gsave 10 dict begin
-239 123 moveto (Toplevel) 49 14.00 -0.50 alignedtext
+247 123 moveto (Toplevel) 49 14.00 -0.50 alignedtext
end grestore
end grestore
% Toplevel -> Mltop
-newpath 271 115 moveto
-353 96 570 45 654 26 curveto
+newpath 279 115 moveto
+361 96 578 45 662 26 curveto
stroke
-newpath 651 24 moveto
-661 24 lineto
-652 29 lineto
+newpath 659 24 moveto
+669 24 lineto
+660 29 lineto
closepath
gsave 0 setgray stroke grestore fill
% Protectedtoplevel
gsave 10 dict begin
-369 253 59 18 ellipse_path
+377 253 59 18 ellipse_path
stroke
gsave 10 dict begin
-369 254 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
+377 254 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
end grestore
end grestore
% Toplevel -> Protectedtoplevel
-newpath 255 138 moveto
-278 161 320 204 347 231 curveto
+newpath 263 138 moveto
+286 161 328 204 355 231 curveto
stroke
-newpath 347 227 moveto
-352 236 lineto
-343 231 lineto
+newpath 355 227 moveto
+360 236 lineto
+351 231 lineto
closepath
gsave 0 setgray stroke grestore fill
% Protectedtoplevel -> Vernac
-newpath 421 244 moveto
-446 240 473 236 495 232 curveto
+newpath 429 244 moveto
+454 240 481 236 503 232 curveto
stroke
-newpath 494 230 moveto
-504 231 lineto
-494 235 lineto
+newpath 502 230 moveto
+512 231 lineto
+502 235 lineto
closepath
gsave 0 setgray stroke grestore fill
% Errors
gsave 10 dict begin
-534 280 27 18 ellipse_path
+542 280 27 18 ellipse_path
stroke
gsave 10 dict begin
-534 281 moveto (Errors) 34 14.00 -0.50 alignedtext
+542 281 moveto (Errors) 34 14.00 -0.50 alignedtext
end grestore
end grestore
% Protectedtoplevel -> Errors
-newpath 421 262 moveto
-447 266 476 271 499 274 curveto
+newpath 429 262 moveto
+455 266 484 271 507 274 curveto
stroke
-newpath 497 271 moveto
-507 275 lineto
-497 276 lineto
+newpath 505 271 moveto
+515 275 lineto
+505 276 lineto
closepath
gsave 0 setgray stroke grestore fill
% Line_oriented_parser
gsave 10 dict begin
-534 334 70 18 ellipse_path
+542 334 70 18 ellipse_path
stroke
gsave 10 dict begin
-534 335 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
+542 335 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
end grestore
end grestore
% Protectedtoplevel -> Line_oriented_parser
-newpath 395 269 moveto
-416 282 445 300 464 310 curveto
-469 312 476 315 483 318 curveto
+newpath 403 269 moveto
+424 282 453 300 472 310 curveto
+477 312 484 315 491 318 curveto
stroke
-newpath 481 315 moveto
-490 320 lineto
-480 320 lineto
+newpath 489 315 moveto
+498 320 lineto
+488 320 lineto
closepath
gsave 0 setgray stroke grestore fill
% Errors -> Himsg
-newpath 561 278 moveto
-611 274 717 265 773 260 curveto
+newpath 569 278 moveto
+619 274 725 265 781 260 curveto
stroke
-newpath 771 258 moveto
-781 259 lineto
-771 263 lineto
+newpath 779 258 moveto
+789 259 lineto
+779 263 lineto
closepath
gsave 0 setgray stroke grestore fill
% Minicoq
gsave 10 dict begin
-34 230 34 18 ellipse_path
+42 230 34 18 ellipse_path
stroke
gsave 10 dict begin
-34 231 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+42 231 moveto (Minicoq) 47 14.00 -0.50 alignedtext
end grestore
end grestore
% Fhimsg
gsave 10 dict begin
-136 230 31 18 ellipse_path
+144 230 31 18 ellipse_path
stroke
gsave 10 dict begin
-136 231 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
+144 231 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
end grestore
end grestore
% Minicoq -> Fhimsg
-newpath 68 230 moveto
-77 230 86 230 94 230 curveto
+newpath 76 230 moveto
+85 230 94 230 102 230 curveto
stroke
-newpath 94 228 moveto
-104 230 lineto
-94 233 lineto
+newpath 102 228 moveto
+112 230 lineto
+102 233 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coqtop
gsave 10 dict begin
-34 149 31 18 ellipse_path
+42 149 31 18 ellipse_path
stroke
gsave 10 dict begin
-34 150 moveto (Coqtop) 41 14.00 -0.50 alignedtext
+42 150 moveto (Coqtop) 41 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqinit
gsave 10 dict begin
-136 122 31 18 ellipse_path
+144 122 31 18 ellipse_path
stroke
gsave 10 dict begin
-136 123 moveto (Coqinit) 42 14.00 -0.50 alignedtext
+144 123 moveto (Coqinit) 42 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqtop -> Coqinit
-newpath 62 141 moveto
-73 138 86 135 98 132 curveto
+newpath 70 141 moveto
+81 138 94 135 106 132 curveto
stroke
-newpath 97 130 moveto
-107 129 lineto
-98 135 lineto
+newpath 105 130 moveto
+115 129 lineto
+106 135 lineto
closepath
gsave 0 setgray stroke grestore fill
% Usage
gsave 10 dict begin
-136 176 27 18 ellipse_path
+144 176 27 18 ellipse_path
stroke
gsave 10 dict begin
-136 177 moveto (Usage) 34 14.00 -0.50 alignedtext
+144 177 moveto (Usage) 34 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqtop -> Usage
-newpath 62 157 moveto
-74 160 88 164 101 167 curveto
+newpath 70 157 moveto
+82 160 96 164 109 167 curveto
stroke
-newpath 101 164 moveto
-110 169 lineto
-100 169 lineto
+newpath 109 164 moveto
+118 169 lineto
+108 169 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coqinit -> Toplevel
-newpath 168 122 moveto
-176 122 185 122 194 122 curveto
+newpath 176 122 moveto
+184 122 193 122 202 122 curveto
stroke
-newpath 194 120 moveto
-204 122 lineto
-194 125 lineto
+newpath 202 120 moveto
+212 122 lineto
+202 125 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 05:19:00 +0000