aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-14 15:52:54 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-14 15:52:54 +0000
commitfe182e9a9cbf98d3f20bef2ffb4f9c381ccde23a (patch)
treed3de7b8705d435079bf18a992c50314facd4c039 /doc
parent35ab8bf89bb7d879c1114c987ece0b04243c396c (diff)
mise a jour
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1383 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/kernel.dep.ps248
-rw-r--r--doc/library.dep.ps227
-rw-r--r--doc/parsing.dep.ps337
-rw-r--r--doc/preamble.tex1
-rw-r--r--doc/pretyping.dep.ps315
-rw-r--r--doc/proofs.dep.ps182
-rw-r--r--doc/tactics.dep.ps419
-rw-r--r--doc/toplevel.dep.ps368
8 files changed, 1143 insertions, 954 deletions
diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 692a28e87..3604e5ea6 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -3,7 +3,7 @@
%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 576 73
+%%BoundingBox: 36 36 576 91
%%EndComments
%%BeginProlog
save
@@ -139,9 +139,9 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 576 73
+%%PageBoundingBox: 36 36 576 91
gsave
-35 35 541 38 boxprim clip newpath
+35 35 541 56 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0.3994 set_scale
@@ -151,38 +151,38 @@ gsave
% Univ
gsave 10 dict begin
-1229 47 27 18 ellipse_path
+1229 74 27 18 ellipse_path
stroke
gsave 10 dict begin
-1229 48 moveto (Univ) 28 14.00 -0.50 alignedtext
+1229 75 moveto (Univ) 28 14.00 -0.50 alignedtext
end grestore
end grestore
% Names
gsave 10 dict begin
-1322 47 29 18 ellipse_path
+1322 74 29 18 ellipse_path
stroke
gsave 10 dict begin
-1322 48 moveto (Names) 38 14.00 -0.50 alignedtext
+1322 75 moveto (Names) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Univ -> Names
-newpath 1256 47 moveto
-1264 47 1273 47 1282 47 curveto
+newpath 1256 74 moveto
+1264 74 1273 74 1282 74 curveto
stroke
-newpath 1282 45 moveto
-1292 47 lineto
-1282 50 lineto
+newpath 1282 72 moveto
+1292 74 lineto
+1282 77 lineto
closepath
gsave 0 setgray stroke grestore fill
% Typeops
gsave 10 dict begin
-265 45 34 18 ellipse_path
+265 64 34 18 ellipse_path
stroke
gsave 10 dict begin
-265 46 moveto (Typeops) 48 14.00 -0.50 alignedtext
+265 65 moveto (Typeops) 48 14.00 -0.50 alignedtext
end grestore
end grestore
@@ -196,12 +196,12 @@ end grestore
end grestore
% Typeops -> Inductive
-newpath 297 52 moveto
-310 55 325 58 339 62 curveto
+newpath 299 66 moveto
+310 67 323 68 334 69 curveto
stroke
-newpath 339 59 moveto
-348 64 lineto
-338 64 lineto
+newpath 334 67 moveto
+344 70 lineto
+334 71 lineto
closepath
gsave 0 setgray stroke grestore fill
@@ -215,232 +215,262 @@ end grestore
end grestore
% Typeops -> Type_errors
-newpath 297 38 moveto
-308 36 321 33 333 30 curveto
+newpath 292 53 moveto
+306 47 324 41 340 35 curveto
stroke
-newpath 332 28 moveto
-342 27 lineto
-333 33 lineto
+newpath 339 33 moveto
+349 31 lineto
+341 37 lineto
closepath
gsave 0 setgray stroke grestore fill
% Reduction
gsave 10 dict begin
-501 45 39 18 ellipse_path
+501 72 39 18 ellipse_path
stroke
gsave 10 dict begin
-501 46 moveto (Reduction) 57 14.00 -0.50 alignedtext
+501 73 moveto (Reduction) 57 14.00 -0.50 alignedtext
end grestore
end grestore
% Inductive -> Reduction
-newpath 414 64 moveto
-427 61 442 58 456 55 curveto
+newpath 418 72 moveto
+429 72 441 72 452 72 curveto
stroke
-newpath 456 53 moveto
-466 53 lineto
-457 57 lineto
+newpath 452 70 moveto
+462 72 lineto
+452 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Type_errors -> Reduction
-newpath 420 27 moveto
-432 29 444 32 456 35 curveto
+newpath 411 31 moveto
+427 39 448 48 465 55 curveto
stroke
-newpath 456 32 moveto
-465 37 lineto
-455 37 lineto
+newpath 465 52 moveto
+473 59 lineto
+463 57 lineto
closepath
gsave 0 setgray stroke grestore fill
% Closure
gsave 10 dict begin
-608 45 32 18 ellipse_path
+608 72 32 18 ellipse_path
stroke
gsave 10 dict begin
-608 46 moveto (Closure) 43 14.00 -0.50 alignedtext
+608 73 moveto (Closure) 43 14.00 -0.50 alignedtext
end grestore
end grestore
% Reduction -> Closure
-newpath 540 45 moveto
-549 45 558 45 566 45 curveto
+newpath 540 72 moveto
+549 72 558 72 566 72 curveto
stroke
-newpath 566 43 moveto
-576 45 lineto
-566 48 lineto
+newpath 566 70 moveto
+576 72 lineto
+566 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Term
gsave 10 dict begin
-1139 47 27 18 ellipse_path
+1139 74 27 18 ellipse_path
stroke
gsave 10 dict begin
-1139 48 moveto (Term) 30 14.00 -0.50 alignedtext
+1139 75 moveto (Term) 30 14.00 -0.50 alignedtext
end grestore
end grestore
% Term -> Univ
-newpath 1166 47 moveto
-1174 47 1183 47 1192 47 curveto
+newpath 1166 74 moveto
+1174 74 1183 74 1192 74 curveto
stroke
-newpath 1192 45 moveto
-1202 47 lineto
-1192 50 lineto
+newpath 1192 72 moveto
+1202 74 lineto
+1192 77 lineto
closepath
gsave 0 setgray stroke grestore fill
% Sign
gsave 10 dict begin
-1049 47 27 18 ellipse_path
+1049 74 27 18 ellipse_path
stroke
gsave 10 dict begin
-1049 48 moveto (Sign) 25 14.00 -0.50 alignedtext
+1049 75 moveto (Sign) 25 14.00 -0.50 alignedtext
end grestore
end grestore
% Sign -> Term
-newpath 1076 47 moveto
-1084 47 1093 47 1102 47 curveto
+newpath 1076 74 moveto
+1084 74 1093 74 1102 74 curveto
stroke
-newpath 1102 45 moveto
-1112 47 lineto
-1102 50 lineto
+newpath 1102 72 moveto
+1112 74 lineto
+1102 77 lineto
closepath
gsave 0 setgray stroke grestore fill
% Safe_typing
gsave 10 dict begin
-44 45 44 18 ellipse_path
+44 92 44 18 ellipse_path
stroke
gsave 10 dict begin
-44 46 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
+44 93 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
end grestore
end grestore
+% Cooking
+gsave 10 dict begin
+265 118 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+265 119 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
+stroke
+newpath 221 110 moveto
+231 114 lineto
+221 115 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% Indtypes
gsave 10 dict begin
-159 45 34 18 ellipse_path
+159 68 34 18 ellipse_path
stroke
gsave 10 dict begin
-159 46 moveto (Indtypes) 48 14.00 -0.50 alignedtext
+159 69 moveto (Indtypes) 48 14.00 -0.50 alignedtext
end grestore
end grestore
% Safe_typing -> Indtypes
-newpath 88 45 moveto
-97 45 106 45 114 45 curveto
+newpath 83 84 moveto
+94 82 106 79 117 77 curveto
+stroke
+newpath 117 75 moveto
+127 75 lineto
+118 79 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Cooking -> Reduction
+newpath 300 116 moveto
+336 113 393 108 426 102 curveto
+426 102 444 95 462 87 curveto
stroke
-newpath 114 43 moveto
-124 45 lineto
-114 48 lineto
+newpath 461 85 moveto
+471 84 lineto
+462 90 lineto
closepath
gsave 0 setgray stroke grestore fill
% Indtypes -> Typeops
-newpath 194 45 moveto
-203 45 212 45 220 45 curveto
+newpath 193 67 moveto
+203 67 213 66 224 66 curveto
stroke
-newpath 220 43 moveto
-230 45 lineto
-220 48 lineto
+newpath 221 64 moveto
+231 66 lineto
+221 69 lineto
closepath
gsave 0 setgray stroke grestore fill
% Instantiate
gsave 10 dict begin
-716 45 39 18 ellipse_path
+716 72 39 18 ellipse_path
stroke
gsave 10 dict begin
-716 46 moveto (Instantiate) 58 14.00 -0.50 alignedtext
+716 73 moveto (Instantiate) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Closure -> Instantiate
-newpath 640 45 moveto
-648 45 657 45 666 45 curveto
+newpath 640 72 moveto
+648 72 657 72 666 72 curveto
stroke
-newpath 666 43 moveto
-676 45 lineto
-666 48 lineto
+newpath 666 70 moveto
+676 72 lineto
+666 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Environ
gsave 10 dict begin
-825 72 33 18 ellipse_path
+825 99 33 18 ellipse_path
stroke
gsave 10 dict begin
-825 73 moveto (Environ) 45 14.00 -0.50 alignedtext
+825 100 moveto (Environ) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Instantiate -> Environ
-newpath 751 54 moveto
-762 57 774 60 786 62 curveto
+newpath 751 81 moveto
+762 84 774 87 786 89 curveto
stroke
-newpath 786 59 moveto
-795 65 lineto
-785 64 lineto
+newpath 786 86 moveto
+795 92 lineto
+785 91 lineto
closepath
gsave 0 setgray stroke grestore fill
% Evd
gsave 10 dict begin
-940 20 27 18 ellipse_path
+940 47 27 18 ellipse_path
stroke
gsave 10 dict begin
-940 21 moveto (Evd) 22 14.00 -0.50 alignedtext
+940 48 moveto (Evd) 22 14.00 -0.50 alignedtext
end grestore
end grestore
% Instantiate -> Evd
-newpath 755 41 moveto
-797 36 864 29 905 24 curveto
+newpath 755 68 moveto
+797 63 864 56 905 51 curveto
stroke
-newpath 903 22 moveto
-913 23 lineto
-903 27 lineto
+newpath 903 49 moveto
+913 50 lineto
+903 54 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declarations
gsave 10 dict begin
-940 74 45 18 ellipse_path
+940 101 45 18 ellipse_path
stroke
gsave 10 dict begin
-940 75 moveto (Declarations) 70 14.00 -0.50 alignedtext
+940 102 moveto (Declarations) 70 14.00 -0.50 alignedtext
end grestore
end grestore
% Environ -> Declarations
-newpath 858 73 moveto
-866 73 875 73 884 73 curveto
+newpath 858 100 moveto
+866 100 875 100 884 100 curveto
stroke
-newpath 884 71 moveto
-894 73 lineto
-884 76 lineto
+newpath 884 98 moveto
+894 100 lineto
+884 103 lineto
closepath
gsave 0 setgray stroke grestore fill
% Evd -> Sign
-newpath 966 26 moveto
-980 29 998 34 1015 38 curveto
+newpath 966 53 moveto
+980 56 998 61 1015 65 curveto
stroke
-newpath 1015 35 moveto
-1024 41 lineto
-1014 40 lineto
+newpath 1015 62 moveto
+1024 68 lineto
+1014 67 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declarations -> Sign
-newpath 979 64 moveto
-991 62 1003 59 1015 56 curveto
+newpath 979 91 moveto
+991 89 1003 86 1015 83 curveto
stroke
-newpath 1014 54 moveto
-1024 53 lineto
-1015 59 lineto
+newpath 1014 81 moveto
+1024 80 lineto
+1015 86 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index f8995d649..7a5cdeed3 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 519 295
+%%BoundingBox: 36 36 525 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
@@ -139,9 +139,9 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 519 295
+%%PageBoundingBox: 36 36 525 235
gsave
-35 35 484 260 boxprim clip newpath
+35 35 490 200 boxprim clip newpath
36 36 translate
0 0 1 beginpage
0 0 translate 0 rotate
@@ -150,233 +150,220 @@ gsave
% States
gsave 10 dict begin
-27 217 27 18 ellipse_path
+32 180 27 18 ellipse_path
stroke
gsave 10 dict begin
-27 218 moveto (States) 33 14.00 -0.50 alignedtext
+32 181 moveto (States) 33 14.00 -0.50 alignedtext
end grestore
end grestore
% Library
gsave 10 dict begin
-122 217 31 18 ellipse_path
+136 180 31 18 ellipse_path
stroke
gsave 10 dict begin
-122 218 moveto (Library) 41 14.00 -0.50 alignedtext
+136 181 moveto (Library) 41 14.00 -0.50 alignedtext
end grestore
end grestore
% States -> Library
-newpath 54 217 moveto
-62 217 72 217 81 217 curveto
+newpath 59 180 moveto
+70 180 83 180 95 180 curveto
stroke
-newpath 81 215 moveto
-91 217 lineto
-81 220 lineto
+newpath 95 178 moveto
+105 180 lineto
+95 183 lineto
closepath
gsave 0 setgray stroke grestore fill
% Global
gsave 10 dict begin
-334 93 29 18 ellipse_path
+238 180 29 18 ellipse_path
stroke
gsave 10 dict begin
-334 94 moveto (Global) 38 14.00 -0.50 alignedtext
+238 181 moveto (Global) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Library -> Global
-newpath 145 205 moveto
-176 188 231 158 262 140 curveto
-274 132 291 121 306 112 curveto
+newpath 167 180 moveto
+177 180 188 180 198 180 curveto
stroke
-newpath 305 110 moveto
-314 106 lineto
-308 114 lineto
+newpath 198 178 moveto
+208 180 lineto
+198 183 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Goptions
+% Lib
gsave 10 dict begin
-226 240 36 18 ellipse_path
+238 126 27 18 ellipse_path
stroke
gsave 10 dict begin
-226 241 moveto (Goptions) 51 14.00 -0.50 alignedtext
+238 127 moveto (Lib) 19 14.00 -0.50 alignedtext
end grestore
end grestore
-% Library -> Goptions
-newpath 151 223 moveto
-161 225 172 228 183 230 curveto
+% Library -> Lib
+newpath 159 168 moveto
+173 160 193 150 209 141 curveto
stroke
-newpath 184 228 moveto
-193 232 lineto
-183 232 lineto
+newpath 207 139 moveto
+217 137 lineto
+209 144 lineto
closepath
gsave 0 setgray stroke grestore fill
% Nametab
gsave 10 dict begin
-334 20 35 18 ellipse_path
+340 153 35 18 ellipse_path
stroke
gsave 10 dict begin
-334 21 moveto (Nametab) 50 14.00 -0.50 alignedtext
+340 154 moveto (Nametab) 50 14.00 -0.50 alignedtext
end grestore
end grestore
-% Summary
+% Libobject
gsave 10 dict begin
-444 93 37 18 ellipse_path
+450 180 37 18 ellipse_path
stroke
gsave 10 dict begin
-444 94 moveto (Summary) 54 14.00 -0.50 alignedtext
+450 181 moveto (Libobject) 53 14.00 -0.50 alignedtext
end grestore
end grestore
-% Nametab -> Summary
-newpath 356 34 moveto
-373 45 395 61 414 73 curveto
-stroke
-newpath 415 71 moveto
-422 78 lineto
-412 75 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Global -> Summary
-newpath 364 93 moveto
-374 93 385 93 396 93 curveto
+% Nametab -> Libobject
+newpath 372 161 moveto
+383 163 396 166 408 169 curveto
stroke
-newpath 396 91 moveto
-406 93 lineto
-396 96 lineto
+newpath 408 166 moveto
+417 172 lineto
+407 171 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Lib
+% Summary
gsave 10 dict begin
-334 156 27 18 ellipse_path
+450 126 37 18 ellipse_path
stroke
gsave 10 dict begin
-334 157 moveto (Lib) 19 14.00 -0.50 alignedtext
+450 127 moveto (Summary) 54 14.00 -0.50 alignedtext
end grestore
end grestore
-% Goptions -> Lib
-newpath 246 225 moveto
-264 211 290 190 309 175 curveto
+% Nametab -> Summary
+newpath 372 145 moveto
+383 143 395 140 406 137 curveto
stroke
-newpath 306 174 moveto
-316 170 lineto
-309 178 lineto
+newpath 406 134 moveto
+416 134 lineto
+407 139 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Lib -> Summary
-newpath 355 144 moveto
-371 135 393 122 412 112 curveto
+% Global -> Nametab
+newpath 265 173 moveto
+275 170 287 167 298 164 curveto
stroke
-newpath 410 110 moveto
-420 107 lineto
-413 114 lineto
+newpath 298 161 moveto
+308 161 lineto
+299 166 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Libobject
-gsave 10 dict begin
-444 156 37 18 ellipse_path
-stroke
-gsave 10 dict begin
-444 157 moveto (Libobject) 53 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Lib -> Libobject
-newpath 361 156 moveto
-372 156 385 156 397 156 curveto
+% Lib -> Nametab
+newpath 263 133 moveto
+274 136 287 139 299 142 curveto
stroke
-newpath 397 154 moveto
-407 156 lineto
-397 159 lineto
+newpath 299 139 moveto
+308 145 lineto
+298 144 lineto
closepath
gsave 0 setgray stroke grestore fill
% Impargs
gsave 10 dict begin
-226 56 33 18 ellipse_path
+136 126 33 18 ellipse_path
stroke
gsave 10 dict begin
-226 57 moveto (Impargs) 45 14.00 -0.50 alignedtext
+136 127 moveto (Impargs) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Impargs -> Global
-newpath 254 66 moveto
-268 71 285 77 299 81 curveto
+newpath 160 139 moveto
+174 147 192 156 207 164 curveto
stroke
-newpath 299 78 moveto
-308 84 lineto
-298 83 lineto
+newpath 207 161 moveto
+215 168 lineto
+205 166 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Declare
+% Impargs -> Lib
+newpath 169 126 moveto
+180 126 191 126 201 126 curveto
+stroke
+newpath 201 124 moveto
+211 126 lineto
+201 129 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Goptions
gsave 10 dict begin
-122 83 32 18 ellipse_path
+136 72 36 18 ellipse_path
stroke
gsave 10 dict begin
-122 84 moveto (Declare) 43 14.00 -0.50 alignedtext
+136 73 moveto (Goptions) 51 14.00 -0.50 alignedtext
end grestore
end grestore
-% Declare -> Nametab
-newpath 137 67 moveto
-151 52 173 32 190 26 curveto
-217 19 260 18 291 18 curveto
+% Goptions -> Lib
+newpath 161 85 moveto
+175 93 193 102 209 111 curveto
stroke
-newpath 288 16 moveto
-298 18 lineto
-288 21 lineto
+newpath 209 108 moveto
+217 115 lineto
+207 113 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Declare -> Lib
-newpath 137 99 moveto
-151 114 173 134 190 140 curveto
-219 149 267 153 300 155 curveto
+% Declare
+gsave 10 dict begin
+32 72 32 18 ellipse_path
stroke
-newpath 297 153 moveto
-307 155 lineto
-297 158 lineto
-closepath
-gsave 0 setgray stroke grestore fill
+gsave 10 dict begin
+32 73 moveto (Declare) 43 14.00 -0.50 alignedtext
+end grestore
+end grestore
% Declare -> Impargs
-newpath 151 75 moveto
-162 72 175 69 187 66 curveto
+newpath 56 84 moveto
+70 92 88 101 104 110 curveto
stroke
-newpath 186 64 moveto
-196 64 lineto
-187 69 lineto
+newpath 104 107 moveto
+112 114 lineto
+102 112 lineto
closepath
gsave 0 setgray stroke grestore fill
% Indrec
gsave 10 dict begin
-226 110 28 18 ellipse_path
+136 18 28 18 ellipse_path
stroke
gsave 10 dict begin
-226 111 moveto (Indrec) 35 14.00 -0.50 alignedtext
+136 19 moveto (Indrec) 35 14.00 -0.50 alignedtext
end grestore
end grestore
% Declare -> Indrec
-newpath 151 91 moveto
-163 94 178 98 191 101 curveto
+newpath 56 60 moveto
+70 52 90 42 106 33 curveto
stroke
-newpath 191 98 moveto
-200 103 lineto
-190 103 lineto
+newpath 104 31 moveto
+114 29 lineto
+106 36 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 97d69aa0d..5ee8ccaa0 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 217
+%%BoundingBox: 36 36 576 225
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
+ (() show i str cvs show (,) show j str cvs show ()) show
grestore
} if
} bind def
@@ -139,314 +139,367 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 217
+%%PageBoundingBox: 36 36 576 225
gsave
-35 35 542 182 boxprim clip newpath
+35 35 541 190 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.8060 set_scale
+0.7050 set_scale
0 0 translate 0 rotate
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Pcoq
gsave 10 dict begin
-547 110 27 18 ellipse_path
+643 141 27 18 ellipse_path
stroke
gsave 10 dict begin
-547 111 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+643 142 moveto (Pcoq) 28 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqast
gsave 10 dict begin
-640 110 30 18 ellipse_path
+736 141 30 18 ellipse_path
stroke
gsave 10 dict begin
-640 111 moveto (Coqast) 38 14.00 -0.50 alignedtext
+736 142 moveto (Coqast) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Pcoq -> Coqast
-newpath 574 110 moveto
-582 110 591 110 600 110 curveto
+newpath 670 141 moveto
+678 141 687 141 696 141 curveto
stroke
-newpath 600 108 moveto
-610 110 lineto
-600 113 lineto
+newpath 696 139 moveto
+706 141 lineto
+696 144 lineto
closepath
gsave 0 setgray stroke grestore fill
% Extend
gsave 10 dict begin
-364 110 30 18 ellipse_path
+460 141 30 18 ellipse_path
stroke
gsave 10 dict begin
-364 111 moveto (Extend) 39 14.00 -0.50 alignedtext
+460 142 moveto (Extend) 39 14.00 -0.50 alignedtext
end grestore
end grestore
% Ast
gsave 10 dict begin
-457 110 27 18 ellipse_path
+553 141 27 18 ellipse_path
stroke
gsave 10 dict begin
-457 111 moveto (Ast) 19 14.00 -0.50 alignedtext
+553 142 moveto (Ast) 19 14.00 -0.50 alignedtext
end grestore
end grestore
% Extend -> Ast
-newpath 394 110 moveto
-402 110 411 110 420 110 curveto
+newpath 490 141 moveto
+498 141 507 141 516 141 curveto
stroke
-newpath 420 108 moveto
-430 110 lineto
-420 113 lineto
+newpath 516 139 moveto
+526 141 lineto
+516 144 lineto
closepath
gsave 0 setgray stroke grestore fill
% Ast -> Pcoq
-newpath 484 110 moveto
-492 110 501 110 510 110 curveto
+newpath 580 141 moveto
+588 141 597 141 606 141 curveto
stroke
-newpath 510 108 moveto
-520 110 lineto
-510 113 lineto
+newpath 606 139 moveto
+616 141 lineto
+606 144 lineto
closepath
gsave 0 setgray stroke grestore fill
% Termast
gsave 10 dict begin
-258 44 33 18 ellipse_path
+354 195 33 18 ellipse_path
stroke
gsave 10 dict begin
-258 45 moveto (Termast) 45 14.00 -0.50 alignedtext
+354 196 moveto (Termast) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Termast -> Ast
-newpath 285 34 moveto
-317 23 369 9 394 26 curveto
-411 38 430 65 442 85 curveto
+newpath 386 190 moveto
+417 186 463 178 490 171 curveto
+490 171 507 163 523 155 curveto
stroke
-newpath 444 83 moveto
-447 93 lineto
-440 86 lineto
+newpath 521 153 moveto
+531 151 lineto
+523 158 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Pattern
+% Search
gsave 10 dict begin
-364 56 30 18 ellipse_path
+30 60 29 18 ellipse_path
stroke
gsave 10 dict begin
-364 57 moveto (Pattern) 39 14.00 -0.50 alignedtext
+30 61 moveto (Search) 37 14.00 -0.50 alignedtext
end grestore
end grestore
-% Termast -> Pattern
-newpath 290 48 moveto
-301 49 313 50 325 52 curveto
-stroke
-newpath 324 49 moveto
-334 53 lineto
-324 54 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Printer
+% Astterm
gsave 10 dict begin
-136 44 29 18 ellipse_path
+354 33 33 18 ellipse_path
stroke
gsave 10 dict begin
-136 45 moveto (Printer) 38 14.00 -0.50 alignedtext
+354 34 moveto (Astterm) 45 14.00 -0.50 alignedtext
end grestore
end grestore
-% Printer -> Termast
-newpath 166 44 moveto
-181 44 199 44 215 44 curveto
+% Search -> Astterm
+newpath 57 53 moveto
+92 45 151 31 186 26 curveto
+217 22 248 25 278 26 curveto
+288 27 301 28 314 29 curveto
stroke
-newpath 215 42 moveto
-225 44 lineto
-215 47 lineto
+newpath 311 26 moveto
+321 30 lineto
+311 31 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Esyntax
+% Pretty
gsave 10 dict begin
-258 98 33 18 ellipse_path
+123 110 27 18 ellipse_path
stroke
gsave 10 dict begin
-258 99 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+123 111 moveto (Pretty) 33 14.00 -0.50 alignedtext
end grestore
end grestore
-% Printer -> Esyntax
-newpath 160 55 moveto
-178 63 204 74 224 83 curveto
+% Search -> Pretty
+newpath 53 72 moveto
+65 79 80 87 94 94 curveto
stroke
-newpath 224 80 moveto
-232 87 lineto
-222 85 lineto
+newpath 95 92 moveto
+102 99 lineto
+92 96 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Esyntax -> Extend
-newpath 290 102 moveto
-301 103 313 104 325 106 curveto
+% Astterm -> Ast
+newpath 387 35 moveto
+418 38 465 44 490 57 curveto
+509 67 527 95 540 116 curveto
stroke
-newpath 324 103 moveto
-334 107 lineto
-324 108 lineto
+newpath 542 114 moveto
+544 124 lineto
+537 116 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Pretty
+% Printer
gsave 10 dict begin
-27 44 27 18 ellipse_path
+232 164 29 18 ellipse_path
stroke
gsave 10 dict begin
-27 45 moveto (Pretty) 33 14.00 -0.50 alignedtext
+232 165 moveto (Printer) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Pretty -> Printer
-newpath 54 44 moveto
-67 44 82 44 96 44 curveto
+newpath 145 121 moveto
+161 129 183 139 201 149 curveto
stroke
-newpath 96 42 moveto
-106 44 lineto
-96 47 lineto
+newpath 201 146 moveto
+209 153 lineto
+199 151 lineto
closepath
gsave 0 setgray stroke grestore fill
-% G_zsyntax
+% Printer -> Termast
+newpath 259 171 moveto
+275 175 296 180 315 185 curveto
+stroke
+newpath 315 182 moveto
+324 187 lineto
+314 187 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Esyntax
gsave 10 dict begin
-136 152 40 18 ellipse_path
+354 141 33 18 ellipse_path
stroke
gsave 10 dict begin
-136 153 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
+354 142 moveto (Esyntax) 45 14.00 -0.50 alignedtext
end grestore
end grestore
-% G_zsyntax -> Esyntax
-newpath 165 139 moveto
-182 131 206 121 224 113 curveto
+% Printer -> Esyntax
+newpath 260 159 moveto
+276 156 296 152 313 149 curveto
stroke
-newpath 222 111 moveto
-232 109 lineto
-224 116 lineto
+newpath 313 147 moveto
+323 147 lineto
+314 151 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Astterm
+% Esyntax -> Extend
+newpath 387 141 moveto
+398 141 410 141 421 141 curveto
+stroke
+newpath 420 139 moveto
+430 141 lineto
+420 144 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% G_zsyntax
gsave 10 dict begin
-258 152 33 18 ellipse_path
+232 110 40 18 ellipse_path
stroke
gsave 10 dict begin
-258 153 moveto (Astterm) 45 14.00 -0.50 alignedtext
+232 111 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
end grestore
end grestore
% G_zsyntax -> Astterm
-newpath 176 152 moveto
-189 152 203 152 215 152 curveto
+newpath 259 97 moveto
+266 93 273 89 278 86 curveto
+291 77 302 65 314 57 curveto
+317 55 319 54 322 52 curveto
stroke
-newpath 215 150 moveto
-225 152 lineto
-215 155 lineto
+newpath 321 49 moveto
+331 46 lineto
+324 54 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Astterm -> Ast
-newpath 291 150 moveto
-322 149 367 146 394 140 curveto
-394 140 411 132 427 124 curveto
+% G_zsyntax -> Esyntax
+newpath 267 119 moveto
+282 123 300 127 315 131 curveto
stroke
-newpath 425 122 moveto
-435 120 lineto
-427 127 lineto
+newpath 315 128 moveto
+324 133 lineto
+314 133 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% G_rsyntax
+gsave 10 dict begin
+232 56 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+232 57 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% G_rsyntax -> Astterm
+newpath 269 49 moveto
+283 47 299 43 313 41 curveto
+stroke
+newpath 313 39 moveto
+323 39 lineto
+314 43 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Astterm -> Pattern
-newpath 282 139 moveto
-288 136 294 132 298 128 curveto
-313 114 321 94 334 80 curveto
-334 80 336 79 339 77 curveto
+% G_rsyntax -> Esyntax
+newpath 260 69 moveto
+267 72 274 76 278 80 curveto
+292 90 301 106 314 117 curveto
+317 119 319 120 322 122 curveto
stroke
-newpath 337 76 moveto
-346 71 lineto
-340 79 lineto
+newpath 324 120 moveto
+331 128 lineto
+321 125 lineto
closepath
gsave 0 setgray stroke grestore fill
% G_natsyntax
gsave 10 dict begin
-136 98 45 18 ellipse_path
+232 218 45 18 ellipse_path
stroke
gsave 10 dict begin
-136 99 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+232 219 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
end grestore
end grestore
+% G_natsyntax -> Termast
+newpath 273 210 moveto
+286 208 301 205 314 203 curveto
+stroke
+newpath 313 201 moveto
+323 201 lineto
+314 206 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% G_natsyntax -> Esyntax
-newpath 182 98 moveto
-193 98 205 98 216 98 curveto
+newpath 261 204 moveto
+267 200 274 197 278 194 curveto
+291 185 302 173 314 165 curveto
+314 165 318 163 323 159 curveto
stroke
-newpath 215 96 moveto
-225 98 lineto
-215 101 lineto
+newpath 322 157 moveto
+332 154 lineto
+324 161 lineto
closepath
gsave 0 setgray stroke grestore fill
-% G_natsyntax -> Astterm
-newpath 166 111 moveto
-184 119 206 129 224 137 curveto
+% Stdlib
+gsave 10 dict begin
+354 249 27 18 ellipse_path
stroke
-newpath 224 134 moveto
-233 140 lineto
-223 139 lineto
+gsave 10 dict begin
+354 250 moveto (Stdlib) 33 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% G_natsyntax -> Stdlib
+newpath 271 228 moveto
+287 232 305 236 320 240 curveto
+stroke
+newpath 320 237 moveto
+329 243 lineto
+319 242 lineto
closepath
gsave 0 setgray stroke grestore fill
% Egrammar
gsave 10 dict begin
-258 206 40 18 ellipse_path
+354 87 40 18 ellipse_path
stroke
gsave 10 dict begin
-258 207 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+354 88 moveto (Egrammar) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Egrammar -> Extend
-newpath 284 192 moveto
-289 189 295 185 298 182 curveto
-312 170 330 149 344 133 curveto
+newpath 381 101 moveto
+395 109 413 118 429 125 curveto
stroke
-newpath 342 132 moveto
-350 126 lineto
-345 135 lineto
+newpath 429 122 moveto
+437 129 lineto
+427 127 lineto
closepath
gsave 0 setgray stroke grestore fill
% Lexer
gsave 10 dict begin
-364 206 27 18 ellipse_path
+460 87 27 18 ellipse_path
stroke
gsave 10 dict begin
-364 207 moveto (Lexer) 32 14.00 -0.50 alignedtext
+460 88 moveto (Lexer) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Egrammar -> Lexer
-newpath 298 206 moveto
-308 206 318 206 327 206 curveto
+newpath 394 87 moveto
+404 87 414 87 423 87 curveto
stroke
-newpath 327 204 moveto
-337 206 lineto
-327 209 lineto
+newpath 423 85 moveto
+433 87 lineto
+423 90 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/preamble.tex b/doc/preamble.tex
index 75ff1d990..f849ac381 100644
--- a/doc/preamble.tex
+++ b/doc/preamble.tex
@@ -2,6 +2,7 @@
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{ocamlweb}
+\pagestyle{ocamlweb}
\usepackage{fullpage}
\usepackage{epsfig}
\begin{document}
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 9e5348ac4..e18d3dd57 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 188
+%%BoundingBox: 36 36 576 238
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
+ (() show i str cvs show (,) show j str cvs show ()) show
grestore
} if
} bind def
@@ -139,332 +139,321 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 188
+%%PageBoundingBox: 36 36 576 238
gsave
-35 35 542 153 boxprim clip newpath
+35 35 541 203 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6308 set_scale
+0.7219 set_scale
0 0 translate 0 rotate
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Multcase
gsave 10 dict begin
-347 70 36 18 ellipse_path
+347 220 36 18 ellipse_path
stroke
gsave 10 dict begin
-347 71 moveto (Multcase) 51 14.00 -0.50 alignedtext
+347 221 moveto (Multcase) 51 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarutil
gsave 10 dict begin
-460 72 33 18 ellipse_path
+460 220 33 18 ellipse_path
stroke
gsave 10 dict begin
-460 73 moveto (Evarutil) 45 14.00 -0.50 alignedtext
+460 221 moveto (Evarutil) 45 14.00 -0.50 alignedtext
end grestore
end grestore
% Multcase -> Evarutil
-newpath 383 71 moveto
-394 71 406 71 417 71 curveto
+newpath 383 220 moveto
+394 220 406 220 417 220 curveto
stroke
-newpath 417 69 moveto
-427 71 lineto
-417 74 lineto
+newpath 417 218 moveto
+427 220 lineto
+417 223 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pretype_errors
gsave 10 dict begin
-588 72 51 18 ellipse_path
+588 261 51 18 ellipse_path
stroke
gsave 10 dict begin
-588 73 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
+588 262 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarutil -> Pretype_errors
-newpath 493 72 moveto
-503 72 515 72 526 72 curveto
+newpath 489 229 moveto
+504 234 523 240 540 246 curveto
stroke
-newpath 526 70 moveto
-536 72 lineto
-526 75 lineto
+newpath 541 244 moveto
+550 249 lineto
+540 249 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Tacred
+% Syntax_def
gsave 10 dict begin
-712 180 29 18 ellipse_path
+588 207 42 18 ellipse_path
stroke
gsave 10 dict begin
-712 181 moveto (Tacred) 38 14.00 -0.50 alignedtext
+588 208 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
end grestore
end grestore
-% Retyping
+% Rawterm
gsave 10 dict begin
-820 180 36 18 ellipse_path
+712 153 36 18 ellipse_path
stroke
gsave 10 dict begin
-820 181 moveto (Retyping) 51 14.00 -0.50 alignedtext
+712 154 moveto (Rawterm) 51 14.00 -0.50 alignedtext
end grestore
end grestore
-% Tacred -> Retyping
-newpath 742 180 moveto
-752 180 763 180 774 180 curveto
+% Syntax_def -> Rawterm
+newpath 618 194 moveto
+635 186 658 176 676 168 curveto
stroke
-newpath 774 178 moveto
-784 180 lineto
-774 183 lineto
+newpath 675 166 moveto
+685 165 lineto
+676 171 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Syntax_def
+% Recordops
gsave 10 dict begin
-588 126 42 18 ellipse_path
+460 126 40 18 ellipse_path
stroke
gsave 10 dict begin
-588 127 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
+460 127 moveto (Recordops) 59 14.00 -0.50 alignedtext
end grestore
end grestore
-% Rawterm
+% Classops
gsave 10 dict begin
-712 99 36 18 ellipse_path
+588 45 35 18 ellipse_path
stroke
gsave 10 dict begin
-712 100 moveto (Rawterm) 51 14.00 -0.50 alignedtext
+588 46 moveto (Classops) 49 14.00 -0.50 alignedtext
end grestore
end grestore
-% Syntax_def -> Rawterm
-newpath 626 118 moveto
-640 115 655 111 669 108 curveto
-stroke
-newpath 669 106 moveto
-679 106 lineto
-670 110 lineto
+% Recordops -> Classops
+newpath 485 112 moveto
+491 108 496 105 500 102 curveto
+514 92 523 77 536 69 curveto
+540 66 546 64 551 61 curveto
+stroke
+newpath 550 59 moveto
+560 56 lineto
+552 63 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Recordops
-gsave 10 dict begin
-460 222 40 18 ellipse_path
+% Classops -> Rawterm
+newpath 614 57 moveto
+627 63 640 69 640 69 curveto
+656 83 678 109 694 129 curveto
stroke
-gsave 10 dict begin
-460 223 moveto (Recordops) 59 14.00 -0.50 alignedtext
-end grestore
-end grestore
+newpath 695 126 moveto
+699 136 lineto
+691 129 lineto
+closepath
+gsave 0 setgray stroke grestore fill
-% Classops
+% Retyping
gsave 10 dict begin
-588 180 35 18 ellipse_path
+712 72 36 18 ellipse_path
stroke
gsave 10 dict begin
-588 181 moveto (Classops) 49 14.00 -0.50 alignedtext
+712 73 moveto (Retyping) 51 14.00 -0.50 alignedtext
end grestore
end grestore
-% Recordops -> Classops
-newpath 493 211 moveto
-510 206 532 199 549 193 curveto
+% Classops -> Retyping
+newpath 620 52 moveto
+635 55 653 59 669 63 curveto
stroke
-newpath 548 191 moveto
-558 190 lineto
-549 196 lineto
+newpath 670 61 moveto
+679 65 lineto
+669 65 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Classops -> Tacred
-newpath 623 180 moveto
-639 180 657 180 673 180 curveto
+% Tacred
+gsave 10 dict begin
+712 18 29 18 ellipse_path
stroke
-newpath 672 178 moveto
-682 180 lineto
-672 183 lineto
-closepath
-gsave 0 setgray stroke grestore fill
+gsave 10 dict begin
+712 19 moveto (Tacred) 38 14.00 -0.50 alignedtext
+end grestore
+end grestore
-% Classops -> Rawterm
-newpath 615 169 moveto
-625 165 634 160 640 156 curveto
-654 147 672 133 687 121 curveto
+% Classops -> Tacred
+newpath 620 38 moveto
+637 35 657 30 675 26 curveto
stroke
-newpath 685 120 moveto
-694 115 lineto
-688 123 lineto
+newpath 674 24 moveto
+684 24 lineto
+675 29 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pretyping
gsave 10 dict begin
-38 178 37 18 ellipse_path
+38 126 37 18 ellipse_path
stroke
gsave 10 dict begin
-38 179 moveto (Pretyping) 54 14.00 -0.50 alignedtext
+38 127 moveto (Pretyping) 54 14.00 -0.50 alignedtext
end grestore
end grestore
% Cases
gsave 10 dict begin
-139 178 27 18 ellipse_path
+139 126 27 18 ellipse_path
stroke
gsave 10 dict begin
-139 179 moveto (Cases) 32 14.00 -0.50 alignedtext
+139 127 moveto (Cases) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Pretyping -> Cases
-newpath 76 178 moveto
-85 178 94 178 102 178 curveto
+newpath 76 126 moveto
+85 126 94 126 102 126 curveto
stroke
-newpath 102 176 moveto
-112 178 lineto
-102 181 lineto
+newpath 102 124 moveto
+112 126 lineto
+102 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coercion
gsave 10 dict begin
-238 178 36 18 ellipse_path
+238 126 36 18 ellipse_path
stroke
gsave 10 dict begin
-238 179 moveto (Coercion) 51 14.00 -0.50 alignedtext
+238 127 moveto (Coercion) 51 14.00 -0.50 alignedtext
end grestore
end grestore
% Cases -> Coercion
-newpath 166 178 moveto
-174 178 183 178 192 178 curveto
+newpath 166 126 moveto
+174 126 183 126 192 126 curveto
stroke
-newpath 192 176 moveto
-202 178 lineto
-192 181 lineto
+newpath 192 124 moveto
+202 126 lineto
+192 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Pretype_errors -> Rawterm
-newpath 632 82 moveto
-644 84 657 87 669 90 curveto
+newpath 623 248 moveto
+629 244 636 241 640 237 curveto
+656 223 678 197 694 177 curveto
+stroke
+newpath 691 177 moveto
+699 170 lineto
+695 180 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Pattern
+gsave 10 dict begin
+588 153 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+588 154 moveto (Pattern) 39 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Pattern -> Rawterm
+newpath 618 153 moveto
+632 153 650 153 666 153 curveto
stroke
-newpath 670 88 moveto
-679 92 lineto
-669 92 lineto
+newpath 666 151 moveto
+676 153 lineto
+666 156 lineto
closepath
gsave 0 setgray stroke grestore fill
% Evarconv
gsave 10 dict begin
-347 178 37 18 ellipse_path
+347 126 37 18 ellipse_path
stroke
gsave 10 dict begin
-347 179 moveto (Evarconv) 53 14.00 -0.50 alignedtext
+347 127 moveto (Evarconv) 53 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarconv -> Evarutil
-newpath 371 164 moveto
-376 161 381 157 384 154 curveto
-400 140 423 114 440 95 curveto
+newpath 366 142 moveto
+385 157 414 181 435 199 curveto
stroke
-newpath 437 94 moveto
-446 89 lineto
-441 98 lineto
+newpath 436 197 moveto
+442 205 lineto
+433 200 lineto
closepath
gsave 0 setgray stroke grestore fill
% Evarconv -> Recordops
-newpath 376 189 moveto
-390 194 406 200 421 206 curveto
+newpath 384 126 moveto
+392 126 401 126 410 126 curveto
stroke
-newpath 422 204 moveto
-430 210 lineto
-420 208 lineto
+newpath 410 124 moveto
+420 126 lineto
+410 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Typing
gsave 10 dict begin
-460 168 30 18 ellipse_path
+460 72 30 18 ellipse_path
stroke
gsave 10 dict begin
-460 169 moveto (Typing) 40 14.00 -0.50 alignedtext
+460 73 moveto (Typing) 40 14.00 -0.50 alignedtext
end grestore
end grestore
% Evarconv -> Typing
-newpath 384 175 moveto
-396 174 409 173 421 172 curveto
+newpath 373 113 moveto
+389 105 411 95 428 87 curveto
stroke
-newpath 420 170 moveto
-430 171 lineto
-420 175 lineto
+newpath 426 85 moveto
+436 83 lineto
+428 90 lineto
closepath
gsave 0 setgray stroke grestore fill
% Detyping
gsave 10 dict begin
-588 18 36 18 ellipse_path
+588 99 36 18 ellipse_path
stroke
gsave 10 dict begin
-588 19 moveto (Detyping) 52 14.00 -0.50 alignedtext
+588 100 moveto (Detyping) 52 14.00 -0.50 alignedtext
end grestore
end grestore
% Detyping -> Rawterm
-newpath 616 30 moveto
-625 34 634 38 640 42 curveto
-653 51 671 65 687 77 curveto
+newpath 616 111 moveto
+633 119 657 129 676 137 curveto
stroke
-newpath 688 75 moveto
-694 83 lineto
-685 78 lineto
+newpath 677 135 moveto
+685 141 lineto
+675 139 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coercion -> Evarconv
-newpath 274 178 moveto
-282 178 291 178 300 178 curveto
-stroke
-newpath 300 176 moveto
-310 178 lineto
-300 181 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Class
-gsave 10 dict begin
-347 124 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-347 125 moveto (Class) 30 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Class -> Classops
-newpath 374 126 moveto
-408 128 466 133 500 138 curveto
-514 141 524 150 536 156 curveto
-541 158 549 162 556 165 curveto
-stroke
-newpath 554 161 moveto
-562 168 lineto
-552 166 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Class -> Typing
-newpath 370 133 moveto
-386 139 408 147 425 154 curveto
+newpath 274 126 moveto
+282 126 291 126 300 126 curveto
stroke
-newpath 426 152 moveto
-434 158 lineto
-424 156 lineto
+newpath 300 124 moveto
+310 126 lineto
+300 129 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index b8f9a065e..d5d247a2c 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 129
+%%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
@@ -139,193 +139,203 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 129
+%%PageBoundingBox: 36 36 577 125
gsave
-35 35 542 94 boxprim clip newpath
+35 35 542 90 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6444 set_scale
+0.6178 set_scale
0 0 translate 0 rotate
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
+stroke
+gsave 10 dict begin
+159 127 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
% Tacmach
gsave 10 dict begin
-244 72 36 18 ellipse_path
+280 72 36 18 ellipse_path
stroke
gsave 10 dict begin
-244 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
+280 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
+stroke
+newpath 243 86 moveto
+253 84 lineto
+245 90 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% Evar_refiner
gsave 10 dict begin
-362 72 45 18 ellipse_path
+398 72 45 18 ellipse_path
stroke
gsave 10 dict begin
-362 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
+398 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacmach -> Evar_refiner
-newpath 280 72 moveto
-288 72 297 72 306 72 curveto
+newpath 316 72 moveto
+324 72 333 72 342 72 curveto
stroke
-newpath 306 70 moveto
-316 72 lineto
-306 75 lineto
+newpath 342 70 moveto
+352 72 lineto
+342 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Refiner
gsave 10 dict begin
-475 72 31 18 ellipse_path
+511 72 31 18 ellipse_path
stroke
gsave 10 dict begin
-475 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
+511 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
end grestore
end grestore
% Evar_refiner -> Refiner
-newpath 408 72 moveto
-417 72 426 72 434 72 curveto
+newpath 444 72 moveto
+453 72 462 72 470 72 curveto
stroke
-newpath 434 70 moveto
-444 72 lineto
-434 75 lineto
+newpath 470 70 moveto
+480 72 lineto
+470 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacinterp
gsave 10 dict begin
-37 126 37 18 ellipse_path
+37 99 37 18 ellipse_path
stroke
gsave 10 dict begin
-37 127 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
+37 100 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
end grestore
end grestore
-% Macros
+% Tacinterp -> Tactic_debug
+newpath 71 107 moveto
+82 109 95 112 107 115 curveto
+stroke
+newpath 108 113 moveto
+117 117 lineto
+107 117 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Pfedit
gsave 10 dict begin
-141 126 31 18 ellipse_path
+159 72 27 18 ellipse_path
stroke
gsave 10 dict begin
-141 127 moveto (Macros) 41 14.00 -0.50 alignedtext
+159 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
end grestore
end grestore
-% Tacinterp -> Macros
-newpath 74 126 moveto
-83 126 92 126 100 126 curveto
+% Tacinterp -> Pfedit
+newpath 71 91 moveto
+88 88 108 83 124 80 curveto
stroke
-newpath 100 124 moveto
-110 126 lineto
-100 129 lineto
+newpath 123 78 moveto
+133 78 lineto
+124 83 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Macros -> Tacmach
-newpath 164 114 moveto
-177 106 195 97 210 89 curveto
+% Pfedit -> Tacmach
+newpath 186 72 moveto
+200 72 218 72 234 72 curveto
stroke
-newpath 209 87 moveto
-219 85 lineto
-211 91 lineto
+newpath 234 70 moveto
+244 72 lineto
+234 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Logic
gsave 10 dict begin
-569 72 27 18 ellipse_path
+605 72 27 18 ellipse_path
stroke
gsave 10 dict begin
-569 73 moveto (Logic) 32 14.00 -0.50 alignedtext
+605 73 moveto (Logic) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Refiner -> Logic
-newpath 506 72 moveto
-514 72 523 72 532 72 curveto
+newpath 542 72 moveto
+550 72 559 72 568 72 curveto
stroke
-newpath 532 70 moveto
-542 72 lineto
-532 75 lineto
+newpath 568 70 moveto
+578 72 lineto
+568 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Proof_trees
gsave 10 dict begin
-675 72 42 18 ellipse_path
+711 72 42 18 ellipse_path
stroke
gsave 10 dict begin
-675 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
+711 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
end grestore
end grestore
% Logic -> Proof_trees
-newpath 596 72 moveto
-604 72 613 72 622 72 curveto
+newpath 632 72 moveto
+640 72 649 72 658 72 curveto
stroke
-newpath 622 70 moveto
-632 72 lineto
-622 75 lineto
+newpath 658 70 moveto
+668 72 lineto
+658 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Proof_type
gsave 10 dict begin
-796 72 41 18 ellipse_path
+832 72 41 18 ellipse_path
stroke
gsave 10 dict begin
-796 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
+832 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
end grestore
end grestore
% Proof_trees -> Proof_type
-newpath 718 72 moveto
-727 72 736 72 744 72 curveto
-stroke
-newpath 744 70 moveto
-754 72 lineto
-744 75 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Pfedit
-gsave 10 dict begin
-141 72 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-141 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Pfedit -> Tacmach
-newpath 168 72 moveto
-177 72 188 72 198 72 curveto
+newpath 754 72 moveto
+763 72 772 72 780 72 curveto
stroke
-newpath 198 70 moveto
-208 72 lineto
-198 75 lineto
+newpath 780 70 moveto
+790 72 lineto
+780 75 lineto
closepath
gsave 0 setgray stroke grestore fill
% Clenv
gsave 10 dict begin
-141 18 27 18 ellipse_path
+159 18 27 18 ellipse_path
stroke
gsave 10 dict begin
-141 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
+159 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
end grestore
end grestore
% Clenv -> Tacmach
-newpath 162 29 moveto
-176 37 195 46 211 55 curveto
+newpath 181 28 moveto
+198 36 224 48 244 56 curveto
stroke
-newpath 211 52 moveto
-219 59 lineto
-209 57 lineto
+newpath 245 54 moveto
+253 60 lineto
+243 58 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 940e81966..5e8125d5e 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 194
+%%BoundingBox: 36 36 577 193
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
+ (() show i str cvs show (,) show j str cvs show ()) show
grestore
} if
} bind def
@@ -139,396 +139,427 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 194
+%%PageBoundingBox: 36 36 577 193
gsave
-35 35 542 159 boxprim clip newpath
+35 35 542 158 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6618 set_scale
+0.6250 set_scale
0 0 translate 0 rotate
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Termdn
gsave 10 dict begin
-653 202 32 18 ellipse_path
+701 233 32 18 ellipse_path
stroke
gsave 10 dict begin
-653 203 moveto (Termdn) 44 14.00 -0.50 alignedtext
+701 234 moveto (Termdn) 44 14.00 -0.50 alignedtext
end grestore
end grestore
% Dn
gsave 10 dict begin
-771 202 27 18 ellipse_path
+819 233 27 18 ellipse_path
stroke
gsave 10 dict begin
-771 203 moveto (Dn) 17 14.00 -0.50 alignedtext
+819 234 moveto (Dn) 17 14.00 -0.50 alignedtext
end grestore
end grestore
% Termdn -> Dn
-newpath 686 202 moveto
-701 202 719 202 735 202 curveto
+newpath 734 233 moveto
+749 233 767 233 783 233 curveto
stroke
-newpath 734 200 moveto
-744 202 lineto
-734 205 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Tauto
-gsave 10 dict begin
-127 220 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-127 221 moveto (Tauto) 32 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Auto
-gsave 10 dict begin
-217 166 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-217 167 moveto (Auto) 28 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Tauto -> Auto
-newpath 147 208 moveto
-159 201 175 191 189 183 curveto
-stroke
-newpath 187 181 moveto
-197 178 lineto
-190 185 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Hiddentac
-gsave 10 dict begin
-319 114 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-319 115 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Auto -> Hiddentac
-newpath 239 155 moveto
-252 148 269 140 284 132 curveto
-stroke
-newpath 283 130 moveto
-293 128 lineto
-285 134 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-% Dhyp
-gsave 10 dict begin
-319 168 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-319 169 moveto (Dhyp) 31 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-% Auto -> Dhyp
-newpath 244 167 moveto
-256 167 270 167 282 167 curveto
-stroke
-newpath 282 165 moveto
-292 167 lineto
-282 170 lineto
+newpath 782 231 moveto
+792 233 lineto
+782 236 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tactics
gsave 10 dict begin
-545 87 30 18 ellipse_path
+593 110 30 18 ellipse_path
stroke
gsave 10 dict begin
-545 88 moveto (Tactics) 40 14.00 -0.50 alignedtext
+593 111 moveto (Tactics) 40 14.00 -0.50 alignedtext
end grestore
end grestore
% Hipattern
gsave 10 dict begin
-653 114 36 18 ellipse_path
+701 156 36 18 ellipse_path
stroke
gsave 10 dict begin
-653 115 moveto (Hipattern) 52 14.00 -0.50 alignedtext
+701 157 moveto (Hipattern) 52 14.00 -0.50 alignedtext
end grestore
end grestore
% Tactics -> Hipattern
-newpath 573 94 moveto
-584 97 598 100 610 104 curveto
+newpath 618 121 moveto
+631 127 649 134 664 140 curveto
stroke
-newpath 611 102 moveto
-620 106 lineto
-610 106 lineto
+newpath 665 138 moveto
+673 144 lineto
+663 142 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacticals
gsave 10 dict begin
-653 60 35 18 ellipse_path
+701 102 35 18 ellipse_path
stroke
gsave 10 dict begin
-653 61 moveto (Tacticals) 50 14.00 -0.50 alignedtext
+701 103 moveto (Tacticals) 50 14.00 -0.50 alignedtext
end grestore
end grestore
% Tactics -> Tacticals
-newpath 573 80 moveto
-585 77 599 74 612 70 curveto
+newpath 623 108 moveto
+633 107 645 106 656 105 curveto
stroke
-newpath 611 68 moveto
-621 68 lineto
-612 73 lineto
+newpath 656 103 moveto
+666 104 lineto
+656 107 lineto
closepath
gsave 0 setgray stroke grestore fill
% Wcclausenv
gsave 10 dict begin
-771 60 44 18 ellipse_path
+819 102 44 18 ellipse_path
stroke
gsave 10 dict begin
-771 61 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
+819 103 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacticals -> Wcclausenv
-newpath 689 60 moveto
-698 60 707 60 716 60 curveto
+newpath 737 102 moveto
+746 102 755 102 764 102 curveto
stroke
-newpath 716 58 moveto
-726 60 lineto
-716 63 lineto
+newpath 764 100 moveto
+774 102 lineto
+764 105 lineto
closepath
gsave 0 setgray stroke grestore fill
% Tacentries
gsave 10 dict begin
-434 110 39 18 ellipse_path
+482 141 39 18 ellipse_path
stroke
gsave 10 dict begin
-434 111 moveto (Tacentries) 58 14.00 -0.50 alignedtext
+482 142 moveto (Tacentries) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Tacentries -> Tactics
-newpath 470 103 moveto
-482 101 495 98 507 95 curveto
+newpath 516 132 moveto
+529 128 543 124 556 120 curveto
stroke
-newpath 506 93 moveto
-516 93 lineto
-507 98 lineto
+newpath 555 118 moveto
+565 118 lineto
+556 123 lineto
closepath
gsave 0 setgray stroke grestore fill
% Refine
gsave 10 dict begin
-434 18 29 18 ellipse_path
+482 87 29 18 ellipse_path
stroke
gsave 10 dict begin
-434 19 moveto (Refine) 37 14.00 -0.50 alignedtext
+482 88 moveto (Refine) 37 14.00 -0.50 alignedtext
end grestore
end grestore
% Refine -> Tactics
-newpath 455 31 moveto
-473 42 497 57 516 69 curveto
+newpath 510 93 moveto
+523 95 540 99 554 102 curveto
stroke
-newpath 517 67 moveto
-524 74 lineto
-514 71 lineto
+newpath 555 100 moveto
+564 104 lineto
+554 104 lineto
closepath
gsave 0 setgray stroke grestore fill
% Nbtermdn
gsave 10 dict begin
-434 202 38 18 ellipse_path
+482 233 38 18 ellipse_path
stroke
gsave 10 dict begin
-434 203 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
+482 234 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
end grestore
end grestore
% Btermdn
gsave 10 dict begin
-545 202 35 18 ellipse_path
+593 233 35 18 ellipse_path
stroke
gsave 10 dict begin
-545 203 moveto (Btermdn) 49 14.00 -0.50 alignedtext
+593 234 moveto (Btermdn) 49 14.00 -0.50 alignedtext
end grestore
end grestore
% Nbtermdn -> Btermdn
-newpath 473 202 moveto
-482 202 491 202 500 202 curveto
+newpath 521 233 moveto
+530 233 539 233 548 233 curveto
stroke
-newpath 500 200 moveto
-510 202 lineto
-500 205 lineto
+newpath 548 231 moveto
+558 233 lineto
+548 236 lineto
closepath
gsave 0 setgray stroke grestore fill
% Btermdn -> Termdn
-newpath 580 202 moveto
-590 202 601 202 611 202 curveto
+newpath 628 233 moveto
+638 233 649 233 659 233 curveto
stroke
-newpath 610 200 moveto
-620 202 lineto
-610 205 lineto
+newpath 658 231 moveto
+668 233 lineto
+658 236 lineto
closepath
gsave 0 setgray stroke grestore fill
% Leminv
gsave 10 dict begin
-32 112 32 18 ellipse_path
+32 126 32 18 ellipse_path
stroke
gsave 10 dict begin
-32 113 moveto (Leminv) 43 14.00 -0.50 alignedtext
+32 127 moveto (Leminv) 43 14.00 -0.50 alignedtext
end grestore
end grestore
% Inv
gsave 10 dict begin
-127 112 27 18 ellipse_path
+144 126 27 18 ellipse_path
stroke
gsave 10 dict begin
-127 113 moveto (Inv) 18 14.00 -0.50 alignedtext
+144 127 moveto (Inv) 18 14.00 -0.50 alignedtext
end grestore
end grestore
% Leminv -> Inv
-newpath 64 112 moveto
-73 112 82 112 90 112 curveto
+newpath 64 126 moveto
+78 126 94 126 108 126 curveto
stroke
-newpath 90 110 moveto
-100 112 lineto
-90 115 lineto
+newpath 107 124 moveto
+117 126 lineto
+107 129 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 147 124 moveto
-159 131 175 141 189 149 curveto
+newpath 166 137 moveto
+183 145 208 156 227 165 curveto
stroke
-newpath 190 147 moveto
-197 154 lineto
-187 151 lineto
+newpath 228 163 moveto
+236 169 lineto
+226 167 lineto
closepath
gsave 0 setgray stroke grestore fill
% Elim
gsave 10 dict begin
-217 112 27 18 ellipse_path
+258 126 27 18 ellipse_path
stroke
gsave 10 dict begin
-217 113 moveto (Elim) 27 14.00 -0.50 alignedtext
+258 127 moveto (Elim) 27 14.00 -0.50 alignedtext
end grestore
end grestore
% Inv -> Elim
-newpath 154 112 moveto
-162 112 171 112 180 112 curveto
+newpath 171 126 moveto
+186 126 205 126 222 126 curveto
stroke
-newpath 180 110 moveto
-190 112 lineto
-180 115 lineto
+newpath 221 124 moveto
+231 126 lineto
+221 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Equality
gsave 10 dict begin
-319 60 34 18 ellipse_path
+258 62 34 18 ellipse_path
stroke
gsave 10 dict begin
-319 61 moveto (Equality) 47 14.00 -0.50 alignedtext
+258 63 moveto (Equality) 47 14.00 -0.50 alignedtext
end grestore
end grestore
% Inv -> Equality
-newpath 148 101 moveto
-161 93 178 85 190 82 curveto
-213 76 249 69 277 65 curveto
+newpath 165 114 moveto
+183 104 207 91 227 80 curveto
stroke
-newpath 276 63 moveto
-286 64 lineto
-276 68 lineto
+newpath 225 78 moveto
+235 75 lineto
+228 82 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Hiddentac
+gsave 10 dict begin
+367 137 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+367 138 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Auto -> Hiddentac
+newpath 281 171 moveto
+294 165 313 159 328 153 curveto
+stroke
+newpath 327 151 moveto
+337 149 lineto
+329 155 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Dhyp
+gsave 10 dict begin
+367 191 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+367 192 moveto (Dhyp) 31 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Auto -> Dhyp
+newpath 285 183 moveto
+299 185 316 186 330 187 curveto
+stroke
+newpath 330 185 moveto
+340 188 lineto
+330 189 lineto
closepath
gsave 0 setgray stroke grestore fill
% Elim -> Hiddentac
-newpath 244 113 moveto
-252 113 261 113 270 113 curveto
+newpath 285 129 moveto
+295 130 307 131 319 132 curveto
stroke
-newpath 270 111 moveto
-280 113 lineto
-270 116 lineto
+newpath 319 130 moveto
+329 133 lineto
+319 134 lineto
closepath
gsave 0 setgray stroke grestore fill
% Equality -> Tactics
-newpath 352 64 moveto
-393 69 463 77 506 82 curveto
+newpath 291 57 moveto
+347 48 461 36 522 57 curveto
+536 62 555 76 569 89 curveto
stroke
-newpath 505 79 moveto
-515 83 lineto
-505 84 lineto
+newpath 570 87 moveto
+576 95 lineto
+567 90 lineto
closepath
gsave 0 setgray stroke grestore fill
% Hiddentac -> Tacentries
-newpath 358 113 moveto
-367 112 375 112 384 112 curveto
+newpath 406 138 moveto
+415 139 423 139 432 139 curveto
stroke
-newpath 384 110 moveto
-394 111 lineto
-384 114 lineto
+newpath 432 137 moveto
+442 140 lineto
+432 141 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Eqdecide
+gsave 10 dict begin
+144 72 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+144 73 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
+stroke
+newpath 214 64 moveto
+224 65 lineto
+214 68 lineto
closepath
gsave 0 setgray stroke grestore fill
% Eauto
gsave 10 dict begin
-127 166 27 18 ellipse_path
+144 180 27 18 ellipse_path
stroke
gsave 10 dict begin
-127 167 moveto (Eauto) 32 14.00 -0.50 alignedtext
+144 181 moveto (Eauto) 32 14.00 -0.50 alignedtext
end grestore
end grestore
% Eauto -> Auto
-newpath 154 166 moveto
-162 166 171 166 180 166 curveto
+newpath 171 180 moveto
+186 180 205 180 222 180 curveto
stroke
-newpath 180 164 moveto
-190 166 lineto
-180 169 lineto
+newpath 221 178 moveto
+231 180 lineto
+221 183 lineto
closepath
gsave 0 setgray stroke grestore fill
% Dhyp -> Tactics
-newpath 346 165 moveto
-380 160 441 152 474 140 curveto
-488 135 507 121 521 108 curveto
+newpath 394 190 moveto
+429 188 489 183 522 171 curveto
+538 166 558 148 573 133 curveto
stroke
-newpath 519 107 moveto
-528 102 lineto
-522 110 lineto
+newpath 571 132 moveto
+579 126 lineto
+574 135 lineto
closepath
gsave 0 setgray stroke grestore fill
% Dhyp -> Nbtermdn
-newpath 344 175 moveto
-358 179 376 185 392 189 curveto
+newpath 391 200 moveto
+406 205 426 212 442 219 curveto
+stroke
+newpath 442 216 moveto
+451 222 lineto
+441 221 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Autorewrite
+gsave 10 dict begin
+144 18 44 18 ellipse_path
+stroke
+gsave 10 dict begin
+144 19 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
stroke
-newpath 392 186 moveto
-401 192 lineto
-391 191 lineto
+newpath 222 45 moveto
+231 51 lineto
+221 50 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index a57446d80..f1b891887 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 240
+%%BoundingBox: 36 36 577 190
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
+ (() show i str cvs show (,) show j str cvs show ()) show
grestore
} if
} bind def
@@ -139,340 +139,428 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 240
+%%PageBoundingBox: 36 36 577 190
gsave
-35 35 542 205 boxprim clip newpath
+35 35 542 155 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.6683 set_scale
+0.6150 set_scale
0 0 translate 0 rotate
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Vernacinterp
gsave 10 dict begin
-645 180 46 18 ellipse_path
+715 95 46 18 ellipse_path
stroke
gsave 10 dict begin
-645 181 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
+715 96 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
end grestore
end grestore
% Command
gsave 10 dict begin
-768 96 39 18 ellipse_path
+838 124 39 18 ellipse_path
stroke
gsave 10 dict begin
-768 97 moveto (Command) 58 14.00 -0.50 alignedtext
+838 125 moveto (Command) 58 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacinterp -> Command
-newpath 675 166 moveto
-681 163 688 159 692 156 curveto
-706 147 725 131 742 118 curveto
+newpath 755 104 moveto
+767 107 781 110 794 114 curveto
stroke
-newpath 740 117 moveto
-749 112 lineto
-743 120 lineto
+newpath 794 111 moveto
+803 116 lineto
+793 116 lineto
closepath
gsave 0 setgray stroke grestore fill
% Himsg
gsave 10 dict begin
-768 204 29 18 ellipse_path
+838 70 29 18 ellipse_path
stroke
gsave 10 dict begin
-768 205 moveto (Himsg) 37 14.00 -0.50 alignedtext
+838 71 moveto (Himsg) 37 14.00 -0.50 alignedtext
end grestore
end grestore
% Vernacinterp -> Himsg
-newpath 687 188 moveto
-701 190 717 194 731 197 curveto
+newpath 756 87 moveto
+771 84 787 80 801 78 curveto
stroke
-newpath 731 194 moveto
-740 199 lineto
-730 199 lineto
+newpath 800 76 moveto
+810 76 lineto
+801 81 lineto
closepath
gsave 0 setgray stroke grestore fill
% Vernacentries
gsave 10 dict begin
-513 97 49 18 ellipse_path
+253 126 49 18 ellipse_path
stroke
gsave 10 dict begin
-513 98 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
+253 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
end grestore
end grestore
-% Vernacentries -> Vernacinterp
-newpath 536 113 moveto
-554 127 581 145 598 156 curveto
-601 158 603 159 607 161 curveto
+% Metasyntax
+gsave 10 dict begin
+397 126 43 18 ellipse_path
+stroke
+gsave 10 dict begin
+397 127 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Vernacentries -> Metasyntax
+newpath 302 126 moveto
+316 126 331 126 344 126 curveto
stroke
-newpath 608 159 moveto
-616 166 lineto
-606 163 lineto
+newpath 344 124 moveto
+354 126 lineto
+344 129 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Discharge
+% Mltop
gsave 10 dict begin
-645 126 38 18 ellipse_path
+397 72 27 18 ellipse_path
stroke
gsave 10 dict begin
-645 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
+397 73 moveto (Mltop) 34 14.00 -0.50 alignedtext
end grestore
end grestore
-% Vernacentries -> Discharge
-newpath 555 106 moveto
-570 109 586 113 601 116 curveto
+% Vernacentries -> Mltop
+newpath 287 113 moveto
+311 104 342 93 365 84 curveto
stroke
-newpath 601 113 moveto
-610 118 lineto
-600 118 lineto
+newpath 363 82 moveto
+373 81 lineto
+365 87 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Metasyntax
+% Record
gsave 10 dict begin
-645 72 43 18 ellipse_path
+715 149 30 18 ellipse_path
stroke
gsave 10 dict begin
-645 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
+715 150 moveto (Record) 40 14.00 -0.50 alignedtext
end grestore
end grestore
-% Vernacentries -> Metasyntax
-newpath 557 89 moveto
-570 87 583 84 596 81 curveto
+% Vernacentries -> Record
+newpath 289 139 moveto
+312 147 338 156 338 156 curveto
+433 163 598 156 675 152 curveto
stroke
-newpath 596 79 moveto
-606 79 lineto
-597 83 lineto
+newpath 675 150 moveto
+685 151 lineto
+675 154 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Record
+% Vernac
gsave 10 dict begin
-645 18 30 18 ellipse_path
+562 126 30 18 ellipse_path
stroke
gsave 10 dict begin
-645 19 moveto (Record) 40 14.00 -0.50 alignedtext
+562 127 moveto (Vernac) 40 14.00 -0.50 alignedtext
end grestore
end grestore
-% Vernacentries -> Record
-newpath 537 81 moveto
-556 69 582 52 598 42 curveto
-602 39 609 36 615 33 curveto
+% Metasyntax -> Vernac
+newpath 440 126 moveto
+466 126 498 126 522 126 curveto
stroke
-newpath 611 32 moveto
-621 30 lineto
-613 37 lineto
+newpath 521 124 moveto
+531 126 lineto
+521 129 lineto
closepath
gsave 0 setgray stroke grestore fill
% Record -> Command
-newpath 669 29 moveto
-677 34 686 38 692 42 curveto
-706 51 724 63 739 75 curveto
+newpath 744 143 moveto
+758 141 776 137 792 133 curveto
stroke
-newpath 741 73 moveto
-747 81 lineto
-738 77 lineto
+newpath 792 131 moveto
+802 131 lineto
+793 135 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Vernac
+% Record -> Himsg
+newpath 739 138 moveto
+747 133 756 129 762 125 curveto
+776 116 786 103 798 94 curveto
+801 92 804 90 807 88 curveto
+stroke
+newpath 806 85 moveto
+816 82 lineto
+809 90 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Class
gsave 10 dict begin
-513 178 30 18 ellipse_path
+838 178 27 18 ellipse_path
stroke
gsave 10 dict begin
-513 179 moveto (Vernac) 40 14.00 -0.50 alignedtext
+838 179 moveto (Class) 30 14.00 -0.50 alignedtext
end grestore
end grestore
+% Record -> Class
+newpath 744 156 moveto
+762 160 784 165 803 170 curveto
+stroke
+newpath 803 167 moveto
+812 172 lineto
+802 172 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
% Vernac -> Vernacinterp
-newpath 544 178 moveto
-557 178 573 179 588 179 curveto
+newpath 591 120 moveto
+612 116 640 110 665 105 curveto
stroke
-newpath 588 177 moveto
-598 179 lineto
-588 182 lineto
+newpath 664 103 moveto
+674 103 lineto
+665 108 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Toplevel
+% Discharge
gsave 10 dict begin
-239 232 35 18 ellipse_path
+715 203 38 18 ellipse_path
stroke
gsave 10 dict begin
-239 233 moveto (Toplevel) 49 14.00 -0.50 alignedtext
+715 204 moveto (Discharge) 56 14.00 -0.50 alignedtext
end grestore
end grestore
-% Mltop
+% Vernac -> Discharge
+newpath 585 138 moveto
+611 151 654 172 683 187 curveto
+stroke
+newpath 681 183 moveto
+689 190 lineto
+679 188 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Discharge -> Class
+newpath 751 196 moveto
+767 193 786 189 803 185 curveto
+stroke
+newpath 802 183 moveto
+812 183 lineto
+803 188 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Recordobj
gsave 10 dict begin
-369 259 27 18 ellipse_path
+838 232 39 18 ellipse_path
stroke
gsave 10 dict begin
-369 260 moveto (Mltop) 34 14.00 -0.50 alignedtext
+838 233 moveto (Recordobj) 58 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Discharge -> Recordobj
+newpath 750 211 moveto
+763 214 779 218 793 222 curveto
+stroke
+newpath 793 219 moveto
+802 224 lineto
+792 224 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Toplevel
+gsave 10 dict begin
+253 45 35 18 ellipse_path
+stroke
+gsave 10 dict begin
+253 46 moveto (Toplevel) 49 14.00 -0.50 alignedtext
end grestore
end grestore
% Toplevel -> Mltop
-newpath 271 239 moveto
-290 243 314 248 334 252 curveto
+newpath 286 51 moveto
+309 55 339 61 361 65 curveto
stroke
-newpath 334 249 moveto
-343 254 lineto
-333 254 lineto
+newpath 361 62 moveto
+370 67 lineto
+360 67 lineto
closepath
gsave 0 setgray stroke grestore fill
% Protectedtoplevel
gsave 10 dict begin
-369 205 59 18 ellipse_path
+397 18 59 18 ellipse_path
stroke
gsave 10 dict begin
-369 206 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
+397 19 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
end grestore
end grestore
% Toplevel -> Protectedtoplevel
-newpath 271 225 moveto
-283 223 297 220 310 217 curveto
+newpath 286 39 moveto
+301 36 320 33 337 30 curveto
stroke
-newpath 310 215 moveto
-320 215 lineto
-311 219 lineto
+newpath 337 28 moveto
+347 28 lineto
+338 32 lineto
closepath
gsave 0 setgray stroke grestore fill
% Protectedtoplevel -> Vernac
-newpath 419 196 moveto
-438 193 458 188 475 185 curveto
-stroke
-newpath 474 183 moveto
-484 184 lineto
-474 188 lineto
+newpath 435 32 moveto
+443 34 450 37 456 42 curveto
+474 58 474 88 492 102 curveto
+500 107 512 112 523 116 curveto
+stroke
+newpath 524 114 moveto
+533 119 lineto
+523 119 lineto
closepath
gsave 0 setgray stroke grestore fill
% Errors
gsave 10 dict begin
-513 232 27 18 ellipse_path
+562 18 27 18 ellipse_path
stroke
gsave 10 dict begin
-513 233 moveto (Errors) 34 14.00 -0.50 alignedtext
+562 19 moveto (Errors) 34 14.00 -0.50 alignedtext
end grestore
end grestore
% Protectedtoplevel -> Errors
-newpath 419 214 moveto
-439 217 460 222 478 225 curveto
+newpath 456 18 moveto
+479 18 505 18 525 18 curveto
+stroke
+newpath 524 16 moveto
+534 18 lineto
+524 21 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Line_oriented_parser
+gsave 10 dict begin
+562 72 70 18 ellipse_path
+stroke
+gsave 10 dict begin
+562 73 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+% Protectedtoplevel -> Line_oriented_parser
+newpath 437 31 moveto
+459 38 486 47 510 55 curveto
stroke
-newpath 477 222 moveto
-486 227 lineto
-476 227 lineto
+newpath 510 52 moveto
+519 58 lineto
+509 57 lineto
closepath
gsave 0 setgray stroke grestore fill
% Errors -> Himsg
-newpath 540 229 moveto
-587 224 681 214 732 208 curveto
+newpath 588 23 moveto
+639 33 747 53 803 64 curveto
stroke
-newpath 729 206 moveto
-739 207 lineto
-729 211 lineto
+newpath 800 61 moveto
+810 65 lineto
+800 66 lineto
closepath
gsave 0 setgray stroke grestore fill
% Minicoq
gsave 10 dict begin
-34 286 34 18 ellipse_path
+34 153 34 18 ellipse_path
stroke
gsave 10 dict begin
-34 287 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+34 154 moveto (Minicoq) 47 14.00 -0.50 alignedtext
end grestore
end grestore
% Fhimsg
gsave 10 dict begin
-136 286 31 18 ellipse_path
+136 153 31 18 ellipse_path
stroke
gsave 10 dict begin
-136 287 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
+136 154 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
end grestore
end grestore
% Minicoq -> Fhimsg
-newpath 68 286 moveto
-77 286 86 286 94 286 curveto
+newpath 68 153 moveto
+77 153 86 153 94 153 curveto
stroke
-newpath 94 284 moveto
-104 286 lineto
-94 289 lineto
+newpath 94 151 moveto
+104 153 lineto
+94 156 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coqtop
gsave 10 dict begin
-34 205 31 18 ellipse_path
+34 72 31 18 ellipse_path
stroke
gsave 10 dict begin
-34 206 moveto (Coqtop) 41 14.00 -0.50 alignedtext
+34 73 moveto (Coqtop) 41 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqinit
gsave 10 dict begin
-136 232 31 18 ellipse_path
+136 45 31 18 ellipse_path
stroke
gsave 10 dict begin
-136 233 moveto (Coqinit) 42 14.00 -0.50 alignedtext
+136 46 moveto (Coqinit) 42 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqtop -> Coqinit
-newpath 62 213 moveto
-73 216 86 219 98 222 curveto
+newpath 62 64 moveto
+73 61 86 58 98 55 curveto
stroke
-newpath 98 219 moveto
-107 225 lineto
-97 224 lineto
+newpath 97 53 moveto
+107 52 lineto
+98 58 lineto
closepath
gsave 0 setgray stroke grestore fill
% Usage
gsave 10 dict begin
-136 178 27 18 ellipse_path
+136 99 27 18 ellipse_path
stroke
gsave 10 dict begin
-136 179 moveto (Usage) 34 14.00 -0.50 alignedtext
+136 100 moveto (Usage) 34 14.00 -0.50 alignedtext
end grestore
end grestore
% Coqtop -> Usage
-newpath 62 197 moveto
-74 194 88 190 101 187 curveto
+newpath 62 80 moveto
+74 83 88 87 101 90 curveto
stroke
-newpath 100 185 moveto
-110 185 lineto
-101 190 lineto
+newpath 101 87 moveto
+110 92 lineto
+100 92 lineto
closepath
gsave 0 setgray stroke grestore fill
% Coqinit -> Toplevel
-newpath 168 232 moveto
-176 232 185 232 194 232 curveto
+newpath 168 45 moveto
+180 45 195 45 208 45 curveto
stroke
-newpath 194 230 moveto
-204 232 lineto
-194 235 lineto
+newpath 208 43 moveto
+218 45 lineto
+208 48 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 01:47:13 +0000