documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@245 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 996 insertions, 611 deletions

diff --git a/doc/Makefile b/doc/Makefile
index 09ab4276b..2ba39b97d 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -9,9 +9,10 @@ coq.dvi: coq.tex
 coq.tex::
 	make -C .. doc/coq.tex
 
-depend: kernel.dep.ps library.dep.ps
+depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
+         proofs.dep.ps tactics.dep.ps toplevel.dep.ps
 
-%.dot:
+%.dot: ../%
 	(cd ../$*; ocamldep *.ml *.mli) | ocamldot -lr > $@
 
 %.dep.ps: %.dot
diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 1a694e765..8a9253ae9 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: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 131
+%%BoundingBox: 36 36 577 94
 %%EndComments
 %%BeginProlog
 save
@@ -139,408 +139,385 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 131
+%%PageBoundingBox: 36 36 577 94
 gsave
-35 35 542 96 boxprim clip newpath
+35 35 542 59 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.4787 set_scale
+0.4000 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Univ
 gsave 10 dict begin
-999 98 27 18 ellipse_path
+1221 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-999 99 moveto (Univ) 28 14.00 -0.50 alignedtext
+1221 73 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1098 71 29 18 ellipse_path
+1320 45 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1098 72 moveto (Names) 38 14.00 -0.50 alignedtext
+1320 46 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1024 91 moveto
-1036 88 1049 84 1062 81 curveto
+newpath 1246 65 moveto
+1258 62 1271 58 1284 55 curveto
 stroke
-newpath 1061 79 moveto
-1071 78 lineto
-1062 84 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Typing
-gsave 10 dict begin
-31 98 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-31 99 moveto (Typing) 40 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Indtypes
-gsave 10 dict begin
-133 125 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-133 126 moveto (Indtypes) 48 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Typing -> Indtypes
-newpath 59 105 moveto
-69 108 81 111 92 114 curveto
-stroke
-newpath 93 112 moveto
-102 117 lineto
-92 117 lineto
+newpath 1283 53 moveto
+1293 52 lineto
+1284 58 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Typeops
 gsave 10 dict begin
-133 71 34 18 ellipse_path
+265 70 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-133 72 moveto (Typeops) 48 14.00 -0.50 alignedtext
+265 71 moveto (Typeops) 48 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Typing -> Typeops
-newpath 59 91 moveto
-69 88 81 85 92 82 curveto
-stroke
-newpath 92 79 moveto
-102 79 lineto
-93 84 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
 %	Reduction
 gsave 10 dict begin
-243 125 39 18 ellipse_path
+375 97 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-243 126 moveto (Reduction) 57 14.00 -0.50 alignedtext
+375 98 moveto (Reduction) 57 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Indtypes -> Reduction
-newpath 168 125 moveto
-176 125 185 125 194 125 curveto
-stroke
-newpath 194 123 moveto
-204 125 lineto
-194 128 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
 %	Typeops -> Reduction
-newpath 158 83 moveto
-173 91 192 100 208 108 curveto
+newpath 296 78 moveto
+307 80 319 83 330 86 curveto
 stroke
-newpath 208 105 moveto
-216 112 lineto
-206 110 lineto
+newpath 331 84 moveto
+340 89 lineto
+330 89 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Type_errors
 gsave 10 dict begin
-363 71 44 18 ellipse_path
+495 45 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-363 72 moveto (Type_errors) 68 14.00 -0.50 alignedtext
+495 46 moveto (Type_errors) 68 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Typeops -> Type_errors
-newpath 168 71 moveto
-205 71 265 71 309 71 curveto
+newpath 299 66 moveto
+337 62 399 55 443 51 curveto
 stroke
-newpath 308 69 moveto
-318 71 lineto
-308 74 lineto
+newpath 442 49 moveto
+452 50 lineto
+442 54 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Closure
 gsave 10 dict begin
-363 125 32 18 ellipse_path
+495 99 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-363 126 moveto (Closure) 43 14.00 -0.50 alignedtext
+495 100 moveto (Closure) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Reduction -> Closure
-newpath 282 125 moveto
-295 125 309 125 321 125 curveto
+newpath 414 98 moveto
+427 98 441 98 453 98 curveto
 stroke
-newpath 321 123 moveto
-331 125 lineto
-321 128 lineto
+newpath 453 96 moveto
+463 98 lineto
+453 101 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Environ
 gsave 10 dict begin
-593 99 33 18 ellipse_path
+815 72 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-593 100 moveto (Environ) 45 14.00 -0.50 alignedtext
+815 73 moveto (Environ) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Type_errors -> Environ
-newpath 406 76 moveto
-447 81 511 89 552 94 curveto
+newpath 539 49 moveto
+601 54 713 63 774 68 curveto
 stroke
-newpath 550 91 moveto
-560 95 lineto
-550 96 lineto
+newpath 772 65 moveto
+782 69 lineto
+772 70 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Inductive
 gsave 10 dict begin
-705 180 36 18 ellipse_path
+927 126 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-705 181 moveto (Inductive) 52 14.00 -0.50 alignedtext
+927 127 moveto (Inductive) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Inductive
-newpath 611 114 moveto
-626 127 648 145 662 156 curveto
-665 158 669 161 674 163 curveto
-stroke
-newpath 673 159 moveto
-680 167 lineto
-670 164 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Evd
-gsave 10 dict begin
-705 126 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-705 127 moveto (Evd) 22 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Environ -> Evd
-newpath 623 106 moveto
-638 109 655 114 670 118 curveto
+newpath 840 84 moveto
+855 92 875 101 892 109 curveto
 stroke
-newpath 670 115 moveto
-679 120 lineto
-669 120 lineto
+newpath 893 107 moveto
+901 113 lineto
+891 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Abstraction
 gsave 10 dict begin
-705 18 43 18 ellipse_path
+927 18 43 18 ellipse_path
 stroke
 gsave 10 dict begin
-705 19 moveto (Abstraction) 65 14.00 -0.50 alignedtext
+927 19 moveto (Abstraction) 65 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Abstraction
-newpath 611 84 moveto
-626 71 648 53 662 42 curveto
-665 40 668 38 672 36 curveto
+newpath 840 60 moveto
+854 53 874 44 890 36 curveto
 stroke
-newpath 668 35 moveto
-678 32 lineto
-671 40 lineto
+newpath 889 34 moveto
+899 32 lineto
+891 38 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Constant
 gsave 10 dict begin
-705 72 35 18 ellipse_path
+927 72 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-705 73 moveto (Constant) 49 14.00 -0.50 alignedtext
+927 73 moveto (Constant) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Constant
-newpath 623 92 moveto
-635 89 650 86 663 82 curveto
+newpath 848 72 moveto
+859 72 871 72 882 72 curveto
 stroke
-newpath 663 80 moveto
-673 80 lineto
-664 84 lineto
+newpath 882 70 moveto
+892 72 lineto
+882 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Term
 gsave 10 dict begin
-903 71 27 18 ellipse_path
+1125 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-903 72 moveto (Term) 30 14.00 -0.50 alignedtext
+1125 46 moveto (Term) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Univ
-newpath 928 78 moveto
-939 81 953 85 965 88 curveto
+newpath 1150 52 moveto
+1161 55 1175 59 1187 62 curveto
 stroke
-newpath 965 85 moveto
-974 91 lineto
-964 90 lineto
+newpath 1187 59 moveto
+1196 65 lineto
+1186 64 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Generic
 gsave 10 dict begin
-999 44 32 18 ellipse_path
+1221 18 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-999 45 moveto (Generic) 44 14.00 -0.50 alignedtext
+1221 19 moveto (Generic) 44 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Generic
-newpath 928 64 moveto
-938 61 949 58 960 55 curveto
+newpath 1150 38 moveto
+1160 35 1171 32 1182 29 curveto
 stroke
-newpath 960 52 moveto
-970 52 lineto
-961 57 lineto
+newpath 1182 26 moveto
+1192 26 lineto
+1183 31 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Generic -> Names
-newpath 1028 52 moveto
-1038 55 1051 58 1062 61 curveto
+newpath 1250 26 moveto
+1260 29 1273 32 1284 35 curveto
 stroke
-newpath 1062 58 moveto
-1071 64 lineto
-1061 63 lineto
+newpath 1284 32 moveto
+1293 38 lineto
+1283 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sosub
 gsave 10 dict begin
-812 31 27 18 ellipse_path
+1034 18 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-812 32 moveto (Sosub) 34 14.00 -0.50 alignedtext
+1034 19 moveto (Sosub) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sosub -> Term
-newpath 835 41 moveto
-846 46 860 52 872 57 curveto
+newpath 1059 26 moveto
+1069 29 1080 32 1091 35 curveto
 stroke
-newpath 872 54 moveto
-880 61 lineto
-870 59 lineto
+newpath 1091 32 moveto
+1100 38 lineto
+1090 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sign
 gsave 10 dict begin
-812 112 27 18 ellipse_path
+1034 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-812 113 moveto (Sign) 25 14.00 -0.50 alignedtext
+1034 73 moveto (Sign) 25 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sign -> Term
-newpath 834 102 moveto
-845 97 859 91 872 85 curveto
+newpath 1059 65 moveto
+1069 62 1080 58 1091 55 curveto
 stroke
-newpath 871 83 moveto
-881 81 lineto
-873 87 lineto
+newpath 1090 53 moveto
+1100 53 lineto
+1091 58 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Safe_typing
+gsave 10 dict begin
+44 70 44 18 ellipse_path
+stroke
+gsave 10 dict begin
+44 71 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Indtypes
+gsave 10 dict begin
+159 70 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+159 71 moveto (Indtypes) 48 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Safe_typing -> Indtypes
+newpath 88 70 moveto
+97 70 106 70 114 70 curveto
+stroke
+newpath 114 68 moveto
+124 70 lineto
+114 73 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Indtypes -> Typeops
+newpath 194 70 moveto
+203 70 212 70 220 70 curveto
+stroke
+newpath 220 68 moveto
+230 70 lineto
+220 73 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Instantiate
 gsave 10 dict begin
-484 123 39 18 ellipse_path
+616 98 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-484 124 moveto (Instantiate) 58 14.00 -0.50 alignedtext
+616 99 moveto (Instantiate) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Closure -> Instantiate
-newpath 395 124 moveto
-407 124 421 124 434 124 curveto
+newpath 527 99 moveto
+539 99 553 98 566 98 curveto
 stroke
-newpath 434 122 moveto
-444 124 lineto
-434 127 lineto
+newpath 566 96 moveto
+576 98 lineto
+566 101 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Instantiate -> Environ
-newpath 520 115 moveto
-530 113 542 110 553 108 curveto
+%	Evd
+gsave 10 dict begin
+719 96 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+719 97 moveto (Evd) 22 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Instantiate -> Evd
+newpath 656 97 moveto
+665 97 674 97 682 97 curveto
 stroke
-newpath 552 106 moveto
-562 106 lineto
-553 111 lineto
+newpath 682 95 moveto
+692 97 lineto
+682 100 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Inductive -> Sign
-newpath 730 167 moveto
-736 163 743 159 748 156 curveto
-754 152 772 140 787 129 curveto
+%	Evd -> Environ
+newpath 744 90 moveto
+754 88 765 85 775 82 curveto
 stroke
-newpath 783 128 moveto
-793 125 lineto
-786 133 lineto
+newpath 775 80 moveto
+785 80 lineto
+776 84 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evd -> Sign
-newpath 732 123 moveto
-745 121 761 119 776 117 curveto
+%	Inductive -> Sign
+newpath 953 113 moveto
+968 105 988 96 1004 87 curveto
 stroke
-newpath 775 115 moveto
-785 115 lineto
-776 120 lineto
+newpath 1002 85 moveto
+1012 83 lineto
+1004 90 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Abstraction -> Sosub
-newpath 746 23 moveto
-756 24 766 25 776 27 curveto
+newpath 970 18 moveto
+979 18 988 18 996 18 curveto
 stroke
-newpath 775 24 moveto
-785 28 lineto
-775 29 lineto
+newpath 996 16 moveto
+1006 18 lineto
+996 21 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Constant -> Sign
-newpath 733 83 moveto
-747 88 765 94 779 100 curveto
+newpath 962 72 moveto
+974 72 986 72 997 72 curveto
 stroke
-newpath 779 97 moveto
-788 103 lineto
-778 102 lineto
+newpath 997 70 moveto
+1007 72 lineto
+997 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index b6c58663f..a6a5fc38d 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: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 423 257
+%%BoundingBox: 36 36 429 419
 %%EndComments
 %%BeginProlog
 save
@@ -139,9 +139,9 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 423 257
+%%PageBoundingBox: 36 36 429 419
 gsave
-35 35 388 222 boxprim clip newpath
+35 35 394 384 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
 0 0 translate 0 rotate
@@ -150,194 +150,252 @@ gsave
 
 %	States
 gsave 10 dict begin
-133 56 27 18 ellipse_path
+136 364 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-133 57 moveto (States) 33 14.00 -0.50 alignedtext
+136 365 moveto (States) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Lib
 gsave 10 dict begin
-238 68 27 18 ellipse_path
+244 264 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-238 69 moveto (Lib) 19 14.00 -0.50 alignedtext
+244 265 moveto (Lib) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	States -> Lib
-newpath 160 59 moveto
-173 61 188 62 202 64 curveto
+newpath 156 352 moveto
+162 348 168 343 172 340 curveto
+187 326 208 303 224 286 curveto
 stroke
-newpath 201 61 moveto
-211 65 lineto
-201 66 lineto
+newpath 222 285 moveto
+230 279 lineto
+225 288 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Summary
 gsave 10 dict begin
-348 133 37 18 ellipse_path
+354 164 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-348 134 moveto (Summary) 54 14.00 -0.50 alignedtext
+354 165 moveto (Summary) 54 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Lib -> Summary
-newpath 258 80 moveto
-275 90 297 103 316 114 curveto
+newpath 260 249 moveto
+279 232 308 205 329 186 curveto
 stroke
-newpath 317 112 moveto
-324 119 lineto
-314 116 lineto
+newpath 327 185 moveto
+336 180 lineto
+330 188 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Libobject
 gsave 10 dict begin
-348 68 37 18 ellipse_path
+354 264 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-348 69 moveto (Libobject) 53 14.00 -0.50 alignedtext
+354 265 moveto (Libobject) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Lib -> Libobject
-newpath 265 68 moveto
-276 68 289 68 301 68 curveto
+newpath 271 264 moveto
+282 264 295 264 307 264 curveto
 stroke
-newpath 301 66 moveto
-311 68 lineto
-301 71 lineto
+newpath 307 262 moveto
+317 264 lineto
+307 267 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Nametab
+%	Redinfo
 gsave 10 dict begin
-238 198 35 18 ellipse_path
+136 164 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-238 199 moveto (Nametab) 50 14.00 -0.50 alignedtext
+136 165 moveto (Redinfo) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Nametab -> Summary
-newpath 261 184 moveto
-277 175 298 162 316 152 curveto
+%	Global
+gsave 10 dict begin
+244 164 29 18 ellipse_path
 stroke
-newpath 314 150 moveto
-324 147 lineto
-317 154 lineto
+gsave 10 dict begin
+244 165 moveto (Global) 38 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Redinfo -> Global
+newpath 169 164 moveto
+180 164 193 164 204 164 curveto
+stroke
+newpath 204 162 moveto
+214 164 lineto
+204 167 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Library
+%	Global -> Summary
+newpath 274 164 moveto
+284 164 295 164 306 164 curveto
+stroke
+newpath 306 162 moveto
+316 164 lineto
+306 167 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Nametab
 gsave 10 dict begin
-133 110 31 18 ellipse_path
+244 87 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-133 111 moveto (Library) 41 14.00 -0.50 alignedtext
+244 88 moveto (Nametab) 50 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Library -> Lib
-newpath 159 100 moveto
-173 94 191 87 205 81 curveto
+%	Nametab -> Summary
+newpath 265 102 moveto
+282 113 306 130 325 144 curveto
 stroke
-newpath 204 79 moveto
-214 77 lineto
-206 83 lineto
+newpath 326 142 moveto
+333 149 lineto
+323 146 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Global
+%	Library
 gsave 10 dict begin
-238 133 29 18 ellipse_path
+136 218 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-238 134 moveto (Global) 38 14.00 -0.50 alignedtext
+136 219 moveto (Library) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Library -> Global
-newpath 162 116 moveto
-174 118 188 121 201 125 curveto
+%	Library -> Lib
+newpath 161 229 moveto
+176 235 196 244 212 251 curveto
 stroke
-newpath 201 122 moveto
-210 127 lineto
-200 127 lineto
+newpath 212 248 moveto
+221 254 lineto
+211 253 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Global -> Summary
-newpath 268 133 moveto
-278 133 289 133 300 133 curveto
+%	Library -> Global
+newpath 160 206 moveto
+175 198 196 188 213 179 curveto
 stroke
-newpath 300 131 moveto
-310 133 lineto
-300 136 lineto
+newpath 211 177 moveto
+221 175 lineto
+213 182 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Impargs
 gsave 10 dict begin
-133 164 33 18 ellipse_path
+136 110 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-133 165 moveto (Impargs) 45 14.00 -0.50 alignedtext
+136 111 moveto (Impargs) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Impargs -> Global
-newpath 162 155 moveto
-174 152 189 147 202 144 curveto
+newpath 161 122 moveto
+176 130 196 140 213 148 curveto
+stroke
+newpath 213 145 moveto
+221 152 lineto
+211 150 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Goptions
+gsave 10 dict begin
+136 310 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+136 311 moveto (Goptions) 51 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Goptions -> Lib
+newpath 164 298 moveto
+179 292 197 284 212 278 curveto
 stroke
-newpath 201 142 moveto
-211 141 lineto
-202 147 lineto
+newpath 211 276 moveto
+221 274 lineto
+213 280 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declare
 gsave 10 dict begin
-32 164 32 18 ellipse_path
+32 87 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-32 165 moveto (Declare) 43 14.00 -0.50 alignedtext
+32 88 moveto (Declare) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Declare -> Lib
-newpath 38 146 moveto
-49 115 74 53 100 26 curveto
-123 3 179 31 212 51 curveto
+newpath 36 105 moveto
+44 140 66 219 100 248 curveto
+123 266 172 268 206 267 curveto
 stroke
-newpath 212 48 moveto
-219 55 lineto
-209 52 lineto
+newpath 207 264 moveto
+217 266 lineto
+207 269 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declare -> Nametab
-newpath 57 175 moveto
-77 184 100 194 100 194 curveto
-124 198 162 199 192 199 curveto
+newpath 64 84 moveto
+76 82 90 81 100 80 curveto
+126 79 168 81 199 83 curveto
 stroke
-newpath 192 197 moveto
-202 199 lineto
-192 202 lineto
+newpath 199 81 moveto
+209 84 lineto
+199 85 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declare -> Impargs
-newpath 64 164 moveto
-72 164 81 164 90 164 curveto
+newpath 62 94 moveto
+73 96 85 99 96 101 curveto
+stroke
+newpath 96 98 moveto
+105 103 lineto
+95 103 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 53 73 moveto
+69 63 91 48 108 36 curveto
 stroke
-newpath 90 162 moveto
-100 164 lineto
-90 167 lineto
+newpath 106 34 moveto
+116 31 lineto
+109 38 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 95be92210..de816c0af 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: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 158
+%%BoundingBox: 36 36 576 183
 %%EndComments
 %%BeginProlog
 save
@@ -139,185 +139,283 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 158
+%%PageBoundingBox: 36 36 576 183
 gsave
-35 35 541 123 boxprim clip newpath
+35 35 541 148 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.8571 set_scale
+0.7988 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
-%	Pcoq
+%	Termast
 gsave 10 dict begin
-507 72 27 18 ellipse_path
+367 160 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-507 73 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+367 161 moveto (Termast) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Coqast
+%	Ast
 gsave 10 dict begin
-600 72 30 18 ellipse_path
+463 83 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-600 73 moveto (Coqast) 38 14.00 -0.50 alignedtext
+463 84 moveto (Ast) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pcoq -> Coqast
-newpath 534 72 moveto
-542 72 551 72 560 72 curveto
+%	Termast -> Ast
+newpath 386 145 moveto
+401 133 422 116 438 103 curveto
 stroke
-newpath 560 70 moveto
-570 72 lineto
-560 75 lineto
+newpath 436 102 moveto
+445 97 lineto
+439 105 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Extend
+%	Pcoq
 gsave 10 dict begin
-321 72 30 18 ellipse_path
+553 83 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-321 73 moveto (Extend) 39 14.00 -0.50 alignedtext
+553 84 moveto (Pcoq) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Ast
+%	Ast -> Pcoq
+newpath 490 83 moveto
+498 83 507 83 516 83 curveto
+stroke
+newpath 516 81 moveto
+526 83 lineto
+516 86 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Printer
 gsave 10 dict begin
-417 72 27 18 ellipse_path
+136 166 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-417 73 moveto (Ast) 19 14.00 -0.50 alignedtext
+136 167 moveto (Printer) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Extend -> Ast
-newpath 351 72 moveto
-360 72 371 72 380 72 curveto
+%	Printer -> Termast
+newpath 166 165 moveto
+206 164 278 162 325 161 curveto
 stroke
-newpath 380 70 moveto
-390 72 lineto
-380 75 lineto
+newpath 324 159 moveto
+334 161 lineto
+324 164 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Ast -> Pcoq
-newpath 444 72 moveto
-452 72 461 72 470 72 curveto
+%	Esyntax
+gsave 10 dict begin
+258 126 33 18 ellipse_path
 stroke
-newpath 470 70 moveto
-480 72 lineto
-470 75 lineto
+gsave 10 dict begin
+258 127 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Printer -> Esyntax
+newpath 162 157 moveto
+179 152 202 144 221 138 curveto
+stroke
+newpath 220 136 moveto
+230 135 lineto
+221 141 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Termast
+%	Extend
 gsave 10 dict begin
-219 124 33 18 ellipse_path
+367 83 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-219 125 moveto (Termast) 45 14.00 -0.50 alignedtext
+367 84 moveto (Extend) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Termast -> Ast
-newpath 251 120 moveto
-282 116 327 109 354 102 curveto
-354 102 371 94 387 86 curveto
+%	Esyntax -> Extend
+newpath 285 115 moveto
+299 110 318 103 333 97 curveto
 stroke
-newpath 385 84 moveto
-395 82 lineto
-387 89 lineto
+newpath 332 95 moveto
+342 93 lineto
+334 99 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Printer
+%	Pretty
 gsave 10 dict begin
-120 97 29 18 ellipse_path
+27 166 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-120 98 moveto (Printer) 38 14.00 -0.50 alignedtext
+27 167 moveto (Pretty) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Printer -> Termast
-newpath 147 104 moveto
-157 107 169 110 180 113 curveto
+%	Pretty -> Printer
+newpath 54 166 moveto
+67 166 82 166 96 166 curveto
 stroke
-newpath 180 110 moveto
-189 116 lineto
-179 115 lineto
+newpath 96 164 moveto
+106 166 lineto
+96 169 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Esyntax
+%	Coqast
 gsave 10 dict begin
-219 70 33 18 ellipse_path
+646 110 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-219 71 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+646 111 moveto (Coqast) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Printer -> Esyntax
-newpath 147 90 moveto
-157 87 169 84 180 81 curveto
+%	Pcoq -> Coqast
+newpath 578 90 moveto
+587 93 599 96 609 99 curveto
 stroke
-newpath 179 79 moveto
-189 78 lineto
-180 84 lineto
+newpath 610 97 moveto
+619 102 lineto
+609 102 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Esyntax -> Extend
-newpath 252 71 moveto
-262 71 272 71 281 71 curveto
+%	Lexer
+gsave 10 dict begin
+646 56 27 18 ellipse_path
 stroke
-newpath 281 69 moveto
-291 71 lineto
-281 74 lineto
+gsave 10 dict begin
+646 57 moveto (Lexer) 32 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Pcoq -> Lexer
+newpath 578 76 moveto
+588 73 601 69 612 66 curveto
+stroke
+newpath 611 64 moveto
+621 63 lineto
+612 69 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Pretty
+%	G_zsyntax
 gsave 10 dict begin
-27 97 27 18 ellipse_path
+136 24 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-27 98 moveto (Pretty) 33 14.00 -0.50 alignedtext
+136 25 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pretty -> Printer
-newpath 54 97 moveto
-62 97 71 97 80 97 curveto
+%	G_zsyntax -> Esyntax
+newpath 158 39 moveto
+167 46 176 53 182 59 curveto
+196 72 204 90 218 102 curveto
+220 104 222 106 225 108 curveto
 stroke
-newpath 80 95 moveto
-90 97 lineto
-80 100 lineto
+newpath 226 106 moveto
+234 113 lineto
+224 110 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Astterm
 gsave 10 dict begin
-321 18 33 18 ellipse_path
+258 18 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-321 19 moveto (Astterm) 45 14.00 -0.50 alignedtext
+258 19 moveto (Astterm) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
+%	G_zsyntax -> Astterm
+newpath 176 22 moveto
+189 21 203 20 215 20 curveto
+stroke
+newpath 215 18 moveto
+225 20 lineto
+215 23 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
 %	Astterm -> Ast
-newpath 344 31 moveto
-357 38 374 48 388 56 curveto
+newpath 289 25 moveto
+321 32 371 44 400 53 curveto
+409 56 421 62 433 67 curveto
+stroke
+newpath 434 65 moveto
+442 72 lineto
+432 69 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	G_natsyntax
+gsave 10 dict begin
+136 89 45 18 ellipse_path
+stroke
+gsave 10 dict begin
+136 90 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	G_natsyntax -> Esyntax
+newpath 172 100 moveto
+187 105 205 110 220 114 curveto
+stroke
+newpath 220 111 moveto
+229 117 lineto
+219 116 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	G_natsyntax -> Astterm
+newpath 162 74 moveto
+181 63 207 47 227 35 curveto
+stroke
+newpath 225 33 moveto
+235 31 lineto
+227 38 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Extend -> Ast
+newpath 397 83 moveto
+406 83 417 83 426 83 curveto
+stroke
+newpath 426 81 moveto
+436 83 lineto
+426 86 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Egrammar
+gsave 10 dict begin
+258 72 40 18 ellipse_path
+stroke
+gsave 10 dict begin
+258 73 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Egrammar -> Extend
+newpath 297 76 moveto
+307 77 318 78 328 79 curveto
 stroke
-newpath 388 53 moveto
-396 60 lineto
-386 58 lineto
+newpath 327 76 moveto
+337 80 lineto
+327 81 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 5840820ab..6a06d166f 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: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 153
+%%BoundingBox: 36 36 576 199
 %%EndComments
 %%BeginProlog
 save
@@ -139,9 +139,9 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 153
+%%PageBoundingBox: 36 36 576 199
 gsave
-35 35 541 118 boxprim clip newpath
+35 35 541 164 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
 0.8207 set_scale
@@ -151,76 +151,123 @@ gsave
 
 %	Multcase
 gsave 10 dict begin
-257 124 36 18 ellipse_path
+257 72 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-257 125 moveto (Multcase) 51 14.00 -0.50 alignedtext
+257 73 moveto (Multcase) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil
 gsave 10 dict begin
-370 124 33 18 ellipse_path
+370 72 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-370 125 moveto (Evarutil) 45 14.00 -0.50 alignedtext
+370 73 moveto (Evarutil) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Multcase -> Evarutil
-newpath 293 124 moveto
-304 124 316 124 327 124 curveto
+newpath 293 72 moveto
+304 72 316 72 327 72 curveto
 stroke
-newpath 327 122 moveto
-337 124 lineto
-327 127 lineto
+newpath 327 70 moveto
+337 72 lineto
+327 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pretype_errors
 gsave 10 dict begin
-498 124 51 18 ellipse_path
+498 45 51 18 ellipse_path
 stroke
 gsave 10 dict begin
-498 125 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
+498 46 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil -> Pretype_errors
-newpath 403 124 moveto
-413 124 425 124 436 124 curveto
+newpath 401 65 moveto
+414 63 429 59 443 56 curveto
 stroke
-newpath 436 122 moveto
-446 124 lineto
-436 127 lineto
+newpath 443 54 moveto
+453 54 lineto
+444 58 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Syntax_def
+gsave 10 dict begin
+498 99 42 18 ellipse_path
+stroke
+gsave 10 dict begin
+498 100 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Rawterm
+gsave 10 dict begin
+622 72 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+622 73 moveto (Rawterm) 51 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Syntax_def -> Rawterm
+newpath 536 91 moveto
+550 88 565 84 579 81 curveto
+stroke
+newpath 579 79 moveto
+589 79 lineto
+580 83 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Recordops
 gsave 10 dict begin
-370 70 40 18 ellipse_path
+370 126 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-370 71 moveto (Recordops) 59 14.00 -0.50 alignedtext
+370 127 moveto (Recordops) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Classops
 gsave 10 dict begin
-498 70 35 18 ellipse_path
+498 153 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-498 71 moveto (Classops) 49 14.00 -0.50 alignedtext
+498 154 moveto (Classops) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Recordops -> Classops
-newpath 410 70 moveto
-424 70 440 70 454 70 curveto
+newpath 406 134 moveto
+422 137 440 141 456 144 curveto
+stroke
+newpath 456 141 moveto
+465 146 lineto
+455 146 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Tacred
+gsave 10 dict begin
+622 153 29 18 ellipse_path
 stroke
-newpath 453 68 moveto
-463 70 lineto
-453 73 lineto
+gsave 10 dict begin
+622 154 moveto (Tacred) 38 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Classops -> Tacred
+newpath 533 153 moveto
+549 153 567 153 583 153 curveto
+stroke
+newpath 582 151 moveto
+592 153 lineto
+582 156 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -233,110 +280,152 @@ gsave 10 dict begin
 end grestore
 end grestore
 
-%	Pretyping -> Multcase
-newpath 65 85 moveto
-81 91 99 99 112 102 curveto
-139 109 183 115 215 119 curveto
+%	Cases
+gsave 10 dict begin
+148 99 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+148 100 moveto (Cases) 32 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Pretyping -> Cases
+newpath 72 80 moveto
+85 83 101 87 114 91 curveto
 stroke
-newpath 212 116 moveto
-222 120 lineto
-212 121 lineto
+newpath 114 88 moveto
+123 93 lineto
+113 93 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coercion
 gsave 10 dict begin
-148 72 36 18 ellipse_path
+148 45 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-148 73 moveto (Coercion) 51 14.00 -0.50 alignedtext
+148 46 moveto (Coercion) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pretyping -> Coercion
-newpath 76 72 moveto
-84 72 93 72 102 72 curveto
+newpath 72 64 moveto
+83 62 95 59 106 56 curveto
 stroke
-newpath 102 70 moveto
-112 72 lineto
-102 75 lineto
+newpath 105 54 moveto
+115 53 lineto
+106 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Retyping
+%	Evarconv
 gsave 10 dict begin
-148 18 36 18 ellipse_path
+257 126 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-148 19 moveto (Retyping) 51 14.00 -0.50 alignedtext
+257 127 moveto (Evarconv) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pretyping -> Retyping
-newpath 64 59 moveto
-79 51 98 42 114 35 curveto
+%	Cases -> Evarconv
+newpath 174 105 moveto
+186 108 201 112 214 116 curveto
 stroke
-newpath 112 33 moveto
-122 31 lineto
-114 38 lineto
+newpath 215 114 moveto
+224 118 lineto
+214 118 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evarconv
+%	Retyping
 gsave 10 dict begin
-257 70 37 18 ellipse_path
+257 18 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-257 71 moveto (Evarconv) 53 14.00 -0.50 alignedtext
+257 19 moveto (Retyping) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
+%	Cases -> Retyping
+newpath 167 86 moveto
+174 82 180 78 184 75 curveto
+197 64 208 52 220 42 curveto
+222 40 225 38 228 36 curveto
+stroke
+newpath 224 35 moveto
+234 32 lineto
+227 40 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
 %	Coercion -> Evarconv
-newpath 184 71 moveto
-192 71 201 71 210 71 curveto
+newpath 170 59 moveto
+176 63 180 66 184 69 curveto
+197 79 208 91 220 102 curveto
+222 104 225 106 228 108 curveto
 stroke
-newpath 210 69 moveto
-220 71 lineto
-210 74 lineto
+newpath 227 104 moveto
+234 112 lineto
+224 109 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Rawterm
-gsave 10 dict begin
-622 124 36 18 ellipse_path
+%	Coercion -> Retyping
+newpath 180 37 moveto
+191 35 204 31 216 28 curveto
 stroke
-gsave 10 dict begin
-622 125 moveto (Rawterm) 51 14.00 -0.50 alignedtext
-end grestore
-end grestore
+newpath 215 26 moveto
+225 26 lineto
+216 31 lineto
+closepath
+gsave 0 setgray stroke grestore fill
 
 %	Pretype_errors -> Rawterm
-newpath 550 124 moveto
-559 124 568 124 576 124 curveto
+newpath 542 55 moveto
+554 57 567 60 579 63 curveto
 stroke
-newpath 576 122 moveto
-586 124 lineto
-576 127 lineto
+newpath 580 61 moveto
+589 65 lineto
+579 65 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evarconv -> Evarutil
-newpath 283 83 moveto
-299 91 320 101 337 108 curveto
+newpath 283 113 moveto
+299 105 320 95 337 88 curveto
 stroke
-newpath 337 105 moveto
-345 112 lineto
-335 110 lineto
+newpath 335 86 moveto
+345 84 lineto
+337 91 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evarconv -> Recordops
-newpath 294 70 moveto
-302 70 311 70 320 70 curveto
+newpath 294 126 moveto
+302 126 311 126 320 126 curveto
+stroke
+newpath 320 124 moveto
+330 126 lineto
+320 129 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Typing
+gsave 10 dict begin
+370 180 30 18 ellipse_path
+stroke
+gsave 10 dict begin
+370 181 moveto (Typing) 40 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Evarconv -> Typing
+newpath 283 139 moveto
+299 147 321 157 338 165 curveto
 stroke
-newpath 320 68 moveto
-330 70 lineto
-320 73 lineto
+newpath 338 162 moveto
+346 169 lineto
+336 167 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index 3152961cb..9f92d1e95 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -3,7 +3,7 @@
 %%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 166
+%%BoundingBox: 36 36 576 145
 %%EndComments
 %%BeginProlog
 save
@@ -139,174 +139,174 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 166
+%%PageBoundingBox: 36 36 576 145
 gsave
-35 35 542 131 boxprim clip newpath
+35 35 541 110 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.9000 set_scale
+0.7521 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
-%	Pfedit
+%	Tacmach
 gsave 10 dict begin
-244 126 27 18 ellipse_path
+244 72 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 127 moveto (Pfedit) 33 14.00 -0.50 alignedtext
+244 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Refiner
+%	Evar_refiner
 gsave 10 dict begin
-357 99 31 18 ellipse_path
+362 72 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-357 100 moveto (Refiner) 41 14.00 -0.50 alignedtext
+362 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Pfedit -> Refiner
-newpath 270 120 moveto
-284 117 302 112 319 108 curveto
+%	Tacmach -> Evar_refiner
+newpath 280 72 moveto
+288 72 297 72 306 72 curveto
 stroke
-newpath 318 106 moveto
-328 106 lineto
-319 111 lineto
+newpath 306 70 moveto
+316 72 lineto
+306 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Logic
+%	Refiner
 gsave 10 dict begin
-451 99 27 18 ellipse_path
+475 72 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-451 100 moveto (Logic) 32 14.00 -0.50 alignedtext
+475 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Refiner -> Logic
-newpath 388 99 moveto
-396 99 405 99 414 99 curveto
+%	Evar_refiner -> Refiner
+newpath 408 72 moveto
+417 72 426 72 434 72 curveto
 stroke
-newpath 414 97 moveto
-424 99 lineto
-414 102 lineto
+newpath 434 70 moveto
+444 72 lineto
+434 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Tacmach
+%	Tacinterp
 gsave 10 dict begin
-126 45 36 18 ellipse_path
+37 126 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-126 46 moveto (Tacmach) 51 14.00 -0.50 alignedtext
+37 127 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Evar_refiner
+%	Macros
 gsave 10 dict begin
-244 72 45 18 ellipse_path
+141 126 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
+141 127 moveto (Macros) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacmach -> Evar_refiner
-newpath 159 53 moveto
-170 55 183 58 195 61 curveto
+%	Tacinterp -> Macros
+newpath 74 126 moveto
+83 126 92 126 100 126 curveto
 stroke
-newpath 195 58 moveto
-204 63 lineto
-194 63 lineto
+newpath 100 124 moveto
+110 126 lineto
+100 129 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Tacred
+%	Macros -> Tacmach
+newpath 164 114 moveto
+177 106 195 97 210 89 curveto
+stroke
+newpath 209 87 moveto
+219 85 lineto
+211 91 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Logic
 gsave 10 dict begin
-244 18 29 18 ellipse_path
+569 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-244 19 moveto (Tacred) 38 14.00 -0.50 alignedtext
+569 73 moveto (Logic) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacmach -> Tacred
-newpath 159 37 moveto
-174 34 192 30 207 26 curveto
-stroke
-newpath 206 24 moveto
-216 24 lineto
-207 29 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Evar_refiner -> Refiner
-newpath 283 81 moveto
-295 84 308 87 319 90 curveto
+%	Refiner -> Logic
+newpath 506 72 moveto
+514 72 523 72 532 72 curveto
 stroke
-newpath 319 87 moveto
-328 92 lineto
-318 92 lineto
+newpath 532 70 moveto
+542 72 lineto
+532 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Proof_trees
 gsave 10 dict begin
-557 126 42 18 ellipse_path
+675 72 42 18 ellipse_path
 stroke
 gsave 10 dict begin
-557 127 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
+675 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Logic -> Proof_trees
-newpath 476 105 moveto
-486 107 499 111 511 114 curveto
+newpath 596 72 moveto
+604 72 613 72 622 72 curveto
 stroke
-newpath 512 112 moveto
-521 116 lineto
-511 116 lineto
+newpath 622 70 moveto
+632 72 lineto
+622 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Typing_ev
+%	Pfedit
 gsave 10 dict begin
-557 72 40 18 ellipse_path
+141 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-557 73 moveto (Typing_ev) 60 14.00 -0.50 alignedtext
+141 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Logic -> Typing_ev
-newpath 476 93 moveto
-487 91 500 87 512 84 curveto
+%	Pfedit -> Tacmach
+newpath 168 72 moveto
+177 72 188 72 198 72 curveto
 stroke
-newpath 512 81 moveto
-522 81 lineto
-513 86 lineto
+newpath 198 70 moveto
+208 72 lineto
+198 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Clenv
 gsave 10 dict begin
-27 45 27 18 ellipse_path
+141 18 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-27 46 moveto (Clenv) 33 14.00 -0.50 alignedtext
+141 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Clenv -> Tacmach
-newpath 54 45 moveto
-62 45 71 45 80 45 curveto
+newpath 162 29 moveto
+176 37 195 46 211 55 curveto
 stroke
-newpath 80 43 moveto
-90 45 lineto
-80 48 lineto
+newpath 211 52 moveto
+219 59 lineto
+209 57 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 058b9275e..0ff40bcdc 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 576 152
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index 55b090edb..28aae6299 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: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 213
+%%BoundingBox: 36 36 576 218
 %%EndComments
 %%BeginProlog
 save
@@ -139,184 +139,346 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 213
+%%PageBoundingBox: 36 36 576 218
 gsave
-35 35 542 178 boxprim clip newpath
+35 35 541 183 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.9278 set_scale
+0.5947 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
-441 118 46 18 ellipse_path
+645 180 46 18 ellipse_path
 stroke
 gsave 10 dict begin
-441 119 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
+645 181 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Himsg
 gsave 10 dict begin
-553 145 29 18 ellipse_path
+757 205 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-553 146 moveto (Himsg) 37 14.00 -0.50 alignedtext
+757 206 moveto (Himsg) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp -> Himsg
-newpath 480 128 moveto
-492 130 505 133 517 136 curveto
+newpath 685 189 moveto
+697 191 709 194 721 197 curveto
 stroke
-newpath 517 133 moveto
-526 138 lineto
-516 138 lineto
+newpath 721 194 moveto
+730 199 lineto
+720 199 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Vernacentries
 gsave 10 dict begin
-309 164 49 18 ellipse_path
+513 126 49 18 ellipse_path
 stroke
 gsave 10 dict begin
-309 165 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
+513 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Vernacinterp
-newpath 345 152 moveto
-361 146 380 139 397 133 curveto
+newpath 546 139 moveto
+563 146 586 155 604 163 curveto
 stroke
-newpath 396 131 moveto
-406 130 lineto
-397 136 lineto
+newpath 605 161 moveto
+613 167 lineto
+603 165 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Command
+gsave 10 dict begin
+645 72 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+645 73 moveto (Command) 58 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Vernacentries -> Command
+newpath 546 113 moveto
+564 105 588 96 607 88 curveto
+stroke
+newpath 606 86 moveto
+616 84 lineto
+608 90 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Discharge
+gsave 10 dict begin
+645 126 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+645 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Vernacentries -> Discharge
+newpath 562 126 moveto
+574 126 585 126 596 126 curveto
+stroke
+newpath 596 124 moveto
+606 126 lineto
+596 129 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Class
+gsave 10 dict begin
+757 97 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+757 98 moveto (Class) 30 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Discharge -> Class
+newpath 679 117 moveto
+693 114 709 110 723 106 curveto
+stroke
+newpath 722 104 moveto
+732 104 lineto
+723 109 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Vernac
 gsave 10 dict begin
-309 72 30 18 ellipse_path
+513 180 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-309 73 moveto (Vernac) 40 14.00 -0.50 alignedtext
+513 181 moveto (Vernac) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernac -> Vernacinterp
-newpath 335 81 moveto
-353 87 377 95 397 103 curveto
+newpath 544 180 moveto
+557 180 573 180 588 180 curveto
 stroke
-newpath 397 100 moveto
-406 106 lineto
-396 105 lineto
+newpath 588 178 moveto
+598 180 lineto
+588 183 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Toplevel
 gsave 10 dict begin
-35 91 35 18 ellipse_path
+239 234 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-35 92 moveto (Toplevel) 49 14.00 -0.50 alignedtext
+239 235 moveto (Toplevel) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Mltop
 gsave 10 dict begin
-165 118 27 18 ellipse_path
+369 261 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-165 119 moveto (Mltop) 34 14.00 -0.50 alignedtext
+369 262 moveto (Mltop) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Mltop
-newpath 67 98 moveto
-86 102 110 107 130 111 curveto
+newpath 271 241 moveto
+290 245 314 250 334 254 curveto
 stroke
-newpath 130 108 moveto
-139 113 lineto
-129 113 lineto
+newpath 334 251 moveto
+343 256 lineto
+333 256 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel
 gsave 10 dict begin
-165 64 59 18 ellipse_path
+369 207 59 18 ellipse_path
 stroke
 gsave 10 dict begin
-165 65 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
+369 208 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Protectedtoplevel
-newpath 67 84 moveto
-79 82 93 79 106 76 curveto
+newpath 271 227 moveto
+283 225 297 222 310 219 curveto
 stroke
-newpath 106 74 moveto
-116 74 lineto
-107 78 lineto
+newpath 310 217 moveto
+320 217 lineto
+311 221 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Mltop -> Vernacinterp
-newpath 193 118 moveto
-238 118 328 118 386 118 curveto
+%	Protectedtoplevel -> Vernac
+newpath 419 198 moveto
+438 195 458 190 475 187 curveto
 stroke
-newpath 384 116 moveto
-394 118 lineto
-384 121 lineto
+newpath 474 185 moveto
+484 186 lineto
+474 190 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Protectedtoplevel -> Vernac
-newpath 223 67 moveto
-239 68 255 69 270 69 curveto
+%	Errors
+gsave 10 dict begin
+513 234 27 18 ellipse_path
 stroke
-newpath 269 66 moveto
-279 70 lineto
-269 71 lineto
+gsave 10 dict begin
+513 235 moveto (Errors) 34 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Protectedtoplevel -> Errors
+newpath 419 216 moveto
+439 219 460 224 478 227 curveto
+stroke
+newpath 477 224 moveto
+486 229 lineto
+476 229 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Errors
+%	Record
 gsave 10 dict begin
-309 18 27 18 ellipse_path
+645 18 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-309 19 moveto (Errors) 34 14.00 -0.50 alignedtext
+645 19 moveto (Record) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Protectedtoplevel -> Errors
-newpath 206 51 moveto
-228 44 255 35 276 29 curveto
+%	Record -> Class
+newpath 670 29 moveto
+678 33 686 38 692 42 curveto
+704 50 721 65 734 76 curveto
+stroke
+newpath 735 74 moveto
+741 82 lineto
+732 77 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Metasyntax
+gsave 10 dict begin
+865 97 43 18 ellipse_path
+stroke
+gsave 10 dict begin
+865 98 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Class -> Metasyntax
+newpath 784 97 moveto
+792 97 802 97 812 97 curveto
 stroke
-newpath 274 27 moveto
-284 26 lineto
-276 32 lineto
+newpath 812 95 moveto
+822 97 lineto
+812 100 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Errors -> Himsg
+newpath 541 231 moveto
+584 225 669 215 718 209 curveto
+stroke
+newpath 718 207 moveto
+728 208 lineto
+718 211 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Minicoq
 gsave 10 dict begin
-441 172 34 18 ellipse_path
+34 288 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+34 289 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Fhimsg
+gsave 10 dict begin
+136 288 31 18 ellipse_path
+stroke
+gsave 10 dict begin
+136 289 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Minicoq -> Fhimsg
+newpath 68 288 moveto
+77 288 86 288 94 288 curveto
+stroke
+newpath 94 286 moveto
+104 288 lineto
+94 291 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Coqtop
+gsave 10 dict begin
+34 207 31 18 ellipse_path
+stroke
+gsave 10 dict begin
+34 208 moveto (Coqtop) 41 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Coqinit
+gsave 10 dict begin
+136 234 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-441 173 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+136 235 moveto (Coqinit) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Minicoq -> Himsg
-newpath 472 164 moveto
-486 161 502 157 517 153 curveto
+%	Coqtop -> Coqinit
+newpath 62 215 moveto
+73 218 86 221 98 224 curveto
+stroke
+newpath 98 221 moveto
+107 227 lineto
+97 226 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Usage
+gsave 10 dict begin
+136 180 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+136 181 moveto (Usage) 34 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Coqtop -> Usage
+newpath 62 199 moveto
+74 196 88 192 101 189 curveto
+stroke
+newpath 100 187 moveto
+110 187 lineto
+101 192 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Coqinit -> Toplevel
+newpath 168 234 moveto
+176 234 185 234 194 234 curveto
 stroke
-newpath 516 151 moveto
-526 151 lineto
-517 156 lineto
+newpath 194 232 moveto
+204 234 lineto
+194 237 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage