MAJ V7.3

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

3 files changed, 375 insertions, 441 deletions

diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index b3ca2ae16..9df862840 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -3,7 +3,7 @@
 %%For: (herbelin) Hugo Herbelin
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 330
+%%BoundingBox: 36 36 576 232
 %%EndComments
 %%BeginProlog
 save
@@ -150,442 +150,379 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 330
+%%PageBoundingBox: 36 36 576 232
 %%PageOrientation: Portrait
 gsave
-35 35 541 295 boxprim clip newpath
+35 35 541 197 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.7479 set_scale
+0.7584 set_scale
 0 0 translate 0 rotate
-[ /CropBox [36 36 576 330] /PAGES pdfmark
+[ /CropBox [36 36 576 232] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Pcoq
 gsave 10 dict begin
-591 251 27 18 ellipse_path
+581 103 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-591 252 moveto (Pcoq) 28 14.00 -0.50 alignedtext
+581 104 moveto (Pcoq) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqast
 gsave 10 dict begin
-684 251 30 18 ellipse_path
+674 103 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-684 252 moveto (Coqast) 38 14.00 -0.50 alignedtext
+674 104 moveto (Coqast) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pcoq -> Coqast
-newpath 618 251 moveto
-626 251 635 251 644 251 curveto
+newpath 608 103 moveto
+616 103 625 103 634 103 curveto
 stroke
-newpath 644 249 moveto
-654 251 lineto
-644 254 lineto
+newpath 634 101 moveto
+644 103 lineto
+634 106 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Extend
 gsave 10 dict begin
-405 224 30 18 ellipse_path
+398 52 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-405 225 moveto (Extend) 39 14.00 -0.50 alignedtext
+398 53 moveto (Extend) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Ast
 gsave 10 dict begin
-501 251 27 18 ellipse_path
+491 103 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-501 252 moveto (Ast) 19 14.00 -0.50 alignedtext
+491 104 moveto (Ast) 19 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Extend -> Ast
-newpath 432 232 moveto
-443 235 455 238 467 241 curveto
+newpath 421 64 moveto
+433 71 448 79 462 86 curveto
 stroke
-newpath 467 238 moveto
-476 244 lineto
-466 243 lineto
+newpath 463 84 moveto
+470 91 lineto
+460 88 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Ast -> Pcoq
-newpath 528 251 moveto
-536 251 545 251 554 251 curveto
+newpath 518 103 moveto
+526 103 535 103 544 103 curveto
 stroke
-newpath 554 249 moveto
-564 251 lineto
-554 254 lineto
+newpath 544 101 moveto
+554 103 lineto
+544 106 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Termast
 gsave 10 dict begin
-405 278 33 18 ellipse_path
+292 156 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-405 279 moveto (Termast) 45 14.00 -0.50 alignedtext
+292 157 moveto (Termast) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Termast -> Ast
-newpath 435 270 moveto
-445 267 456 264 467 261 curveto
+newpath 325 152 moveto
+355 149 401 143 428 136 curveto
+438 133 451 127 462 120 curveto
 stroke
-newpath 466 259 moveto
-476 258 lineto
-467 264 lineto
+newpath 461 118 moveto
+471 115 lineto
+463 122 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Search
 gsave 10 dict begin
-39 305 29 18 ellipse_path
+48 198 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-39 306 moveto (Search) 37 14.00 -0.50 alignedtext
+48 199 moveto (Search) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Astterm
 gsave 10 dict begin
-296 170 33 18 ellipse_path
+170 94 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-296 171 moveto (Astterm) 45 14.00 -0.50 alignedtext
+170 95 moveto (Astterm) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Astterm
-newpath 61 293 moveto
-65 289 69 285 70 281 curveto
-90 199 63 103 106 32 curveto
-126 0 190 10 220 32 curveto
-252 57 237 111 256 146 curveto
-258 149 260 151 263 153 curveto
-stroke
-newpath 264 151 moveto
-272 157 lineto
-262 155 lineto
+newpath 71 186 moveto
+78 183 84 178 88 174 curveto
+104 157 109 133 124 118 curveto
+127 115 132 112 137 109 curveto
+stroke
+newpath 134 108 moveto
+144 106 lineto
+136 112 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqlib
 gsave 10 dict begin
-296 374 29 18 ellipse_path
+292 229 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-296 375 moveto (Coqlib) 38 14.00 -0.50 alignedtext
+292 230 moveto (Coqlib) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Coqlib
-newpath 53 321 moveto
-67 336 88 357 106 362 curveto
-146 372 215 375 257 374 curveto
+newpath 70 210 moveto
+87 218 109 229 124 232 curveto
+159 239 217 235 255 233 curveto
 stroke
-newpath 256 372 moveto
-266 374 lineto
-256 377 lineto
+newpath 253 231 moveto
+263 232 lineto
+253 236 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Printer
 gsave 10 dict begin
-163 278 29 18 ellipse_path
+170 148 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-163 279 moveto (Printer) 38 14.00 -0.50 alignedtext
+170 149 moveto (Printer) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Search -> Printer
-newpath 67 299 moveto
-84 296 107 291 126 286 curveto
+newpath 73 188 moveto
+91 180 116 170 137 162 curveto
 stroke
-newpath 125 284 moveto
-135 284 lineto
-126 289 lineto
+newpath 135 160 moveto
+145 158 lineto
+137 165 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Astterm -> Termast
-newpath 321 182 moveto
-327 186 333 190 336 194 curveto
-352 211 358 235 372 254 curveto
-374 256 376 258 378 260 curveto
-stroke
-newpath 377 256 moveto
-384 264 lineto
-374 261 lineto
+newpath 194 106 moveto
+213 116 239 129 260 139 curveto
+stroke
+newpath 260 136 moveto
+268 143 lineto
+258 141 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Printer -> Termast
-newpath 193 278 moveto
-235 278 314 278 362 278 curveto
+newpath 200 150 moveto
+215 151 233 152 249 153 curveto
 stroke
-newpath 362 276 moveto
-372 278 lineto
-362 281 lineto
+newpath 249 151 moveto
+259 154 lineto
+249 155 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esyntax
 gsave 10 dict begin
-296 224 33 18 ellipse_path
+292 48 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-296 225 moveto (Esyntax) 45 14.00 -0.50 alignedtext
+292 49 moveto (Esyntax) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Printer -> Esyntax
-newpath 188 268 moveto
-208 259 237 247 260 238 curveto
-stroke
-newpath 259 236 moveto
-269 235 lineto
-260 241 lineto
+newpath 194 137 moveto
+203 133 211 128 216 124 curveto
+232 109 238 86 252 72 curveto
+254 70 256 68 259 66 curveto
+stroke
+newpath 258 64 moveto
+268 61 lineto
+260 68 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Esyntax -> Extend
-newpath 329 224 moveto
-340 224 353 224 365 224 curveto
+newpath 325 49 moveto
+336 49 348 50 359 50 curveto
 stroke
-newpath 365 222 moveto
-375 224 lineto
-365 227 lineto
+newpath 358 47 moveto
+368 51 lineto
+358 52 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Prettyp
 gsave 10 dict begin
-39 251 30 18 ellipse_path
+48 144 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-39 252 moveto (Prettyp) 40 14.00 -0.50 alignedtext
+48 145 moveto (Prettyp) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Prettyp -> Printer
-newpath 68 257 moveto
-85 260 107 265 126 270 curveto
+newpath 78 145 moveto
+94 146 114 146 131 147 curveto
 stroke
-newpath 126 267 moveto
-135 272 lineto
-125 272 lineto
+newpath 130 145 moveto
+140 147 lineto
+130 150 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax
 gsave 10 dict begin
-163 224 40 18 ellipse_path
+48 86 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-163 225 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
+48 87 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_zsyntax -> Astterm
-newpath 193 212 moveto
-213 204 240 193 261 184 curveto
+newpath 88 89 moveto
+101 90 115 91 128 91 curveto
 stroke
-newpath 259 182 moveto
-269 181 lineto
-261 187 lineto
+newpath 127 88 moveto
+137 92 lineto
+127 93 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_zsyntax -> Esyntax
-newpath 203 224 moveto
-219 224 237 224 254 224 curveto
-stroke
-newpath 253 222 moveto
-263 224 lineto
-253 227 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	G_string_syntax
-gsave 10 dict begin
-163 170 56 18 ellipse_path
-stroke
-gsave 10 dict begin
-163 171 moveto (G_string_syntax) 92 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	G_string_syntax -> Astterm
-newpath 220 170 moveto
-232 170 243 170 254 170 curveto
-stroke
-newpath 253 168 moveto
-263 170 lineto
-253 173 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	G_string_syntax -> Esyntax
-newpath 198 184 moveto
-217 192 242 202 261 210 curveto
+newpath 80 75 moveto
+95 71 112 66 124 64 curveto
+159 58 214 54 251 51 curveto
 stroke
-newpath 261 207 moveto
-269 213 lineto
-259 212 lineto
+newpath 249 49 moveto
+259 50 lineto
+249 54 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_rsyntax
 gsave 10 dict begin
-163 116 39 18 ellipse_path
+48 25 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-163 117 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
+48 26 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_rsyntax -> Astterm
-newpath 193 128 moveto
-213 136 240 147 261 156 curveto
+newpath 73 39 moveto
+92 50 119 65 139 77 curveto
 stroke
-newpath 261 153 moveto
-269 159 lineto
-259 158 lineto
+newpath 139 74 moveto
+147 81 lineto
+137 79 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_rsyntax -> Esyntax
-newpath 192 128 moveto
-206 134 220 140 220 140 curveto
-238 155 241 182 256 200 curveto
-258 202 260 204 263 206 curveto
-stroke
-newpath 264 204 moveto
-272 211 lineto
-262 208 lineto
+newpath 88 26 moveto
+126 26 182 28 216 31 curveto
+226 32 242 35 255 38 curveto
+stroke
+newpath 253 35 moveto
+262 40 lineto
+252 40 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax
 gsave 10 dict begin
-163 332 45 18 ellipse_path
+170 202 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-163 333 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
+170 203 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	G_natsyntax -> Termast
-newpath 203 323 moveto
-248 313 320 297 365 287 curveto
+newpath 203 190 moveto
+219 184 239 176 256 169 curveto
 stroke
-newpath 364 285 moveto
-374 285 lineto
-365 290 lineto
+newpath 255 167 moveto
+265 166 lineto
+256 172 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax -> Coqlib
-newpath 199 343 moveto
-218 349 242 357 261 363 curveto
+newpath 210 211 moveto
+225 214 241 218 255 221 curveto
 stroke
-newpath 261 360 moveto
-270 366 lineto
-260 365 lineto
+newpath 255 218 moveto
+264 223 lineto
+254 223 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	G_natsyntax -> Esyntax
-newpath 197 320 moveto
-206 316 214 312 220 308 curveto
-238 294 261 267 277 248 curveto
-stroke
-newpath 275 247 moveto
-283 241 lineto
-278 250 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	G_ascii_syntax
-gsave 10 dict begin
-163 62 53 18 ellipse_path
-stroke
-gsave 10 dict begin
-163 63 moveto (G_ascii_syntax) 86 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	G_ascii_syntax -> Astterm
-newpath 201 75 moveto
-209 78 216 82 220 86 curveto
-238 101 241 128 256 146 curveto
-258 148 260 150 263 152 curveto
-stroke
-newpath 264 150 moveto
-272 157 lineto
-262 154 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	G_ascii_syntax -> Esyntax
-newpath 203 74 moveto
-210 77 216 80 220 86 curveto
-243 119 237 165 256 200 curveto
-258 203 260 205 263 207 curveto
-stroke
-newpath 264 205 moveto
-272 211 lineto
-262 209 lineto
+newpath 201 189 moveto
+207 186 213 183 216 178 curveto
+236 146 234 104 252 72 curveto
+252 72 256 70 261 66 curveto
+stroke
+newpath 260 64 moveto
+270 61 lineto
+262 68 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Egrammar
 gsave 10 dict begin
-296 116 40 18 ellipse_path
+292 102 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-296 117 moveto (Egrammar) 58 14.00 -0.50 alignedtext
+292 103 moveto (Egrammar) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Egrammar -> Extend
-newpath 320 131 moveto
-329 136 336 140 336 140 curveto
-351 155 372 181 388 201 curveto
+newpath 320 89 moveto
+334 82 351 74 366 67 curveto
 stroke
-newpath 389 198 moveto
-393 208 lineto
-385 201 lineto
+newpath 364 65 moveto
+374 63 lineto
+366 70 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Lexer
 gsave 10 dict begin
-405 116 27 18 ellipse_path
+398 106 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-405 117 moveto (Lexer) 32 14.00 -0.50 alignedtext
+398 107 moveto (Lexer) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Egrammar -> Lexer
-newpath 336 116 moveto
-347 116 358 116 368 116 curveto
+newpath 332 104 moveto
+342 104 352 105 361 105 curveto
 stroke
-newpath 368 114 moveto
-378 116 lineto
-368 119 lineto
+newpath 361 103 moveto
+371 105 lineto
+361 108 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 8af063428..e6a242ac4 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -3,7 +3,7 @@
 %%For: (herbelin) Hugo Herbelin
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 203
+%%BoundingBox: 36 36 577 201
 %%EndComments
 %%BeginProlog
 save
@@ -150,439 +150,439 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 203
+%%PageBoundingBox: 36 36 577 201
 %%PageOrientation: Portrait
 gsave
-35 35 542 168 boxprim clip newpath
+35 35 542 166 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
 0.4796 set_scale
 0 0 translate 0 rotate
-[ /CropBox [36 36 577 203] /PAGES pdfmark
+[ /CropBox [36 36 577 201] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Multcase
 gsave 10 dict begin
-355 234 36 18 ellipse_path
+355 272 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-355 235 moveto (Multcase) 51 14.00 -0.50 alignedtext
+355 273 moveto (Multcase) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil
 gsave 10 dict begin
-468 234 33 18 ellipse_path
+468 272 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-468 235 moveto (Evarutil) 45 14.00 -0.50 alignedtext
+468 273 moveto (Evarutil) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Multcase -> Evarutil
-newpath 391 234 moveto
-402 234 414 234 425 234 curveto
+newpath 391 272 moveto
+402 272 414 272 425 272 curveto
 stroke
-newpath 425 232 moveto
-435 234 lineto
-425 237 lineto
+newpath 425 270 moveto
+435 272 lineto
+425 275 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pretype_errors
 gsave 10 dict begin
-596 180 51 18 ellipse_path
+596 272 51 18 ellipse_path
 stroke
 gsave 10 dict begin
-596 181 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
+596 273 moveto (Pretype_errors) 82 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil -> Pretype_errors
-newpath 494 223 moveto
-511 216 535 206 554 198 curveto
+newpath 501 272 moveto
+511 272 523 272 534 272 curveto
 stroke
-newpath 553 196 moveto
-563 194 lineto
-555 200 lineto
+newpath 534 270 moveto
+544 272 lineto
+534 275 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Indrec
 gsave 10 dict begin
-596 288 28 18 ellipse_path
+596 326 28 18 ellipse_path
 stroke
 gsave 10 dict begin
-596 289 moveto (Indrec) 35 14.00 -0.50 alignedtext
+596 327 moveto (Indrec) 35 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Evarutil -> Indrec
-newpath 494 245 moveto
-514 254 542 266 564 275 curveto
+newpath 494 283 moveto
+514 292 542 304 564 313 curveto
 stroke
-newpath 564 272 moveto
-572 278 lineto
-562 277 lineto
+newpath 564 310 moveto
+572 316 lineto
+562 315 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Typing
 gsave 10 dict begin
-468 180 30 18 ellipse_path
+468 218 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-468 181 moveto (Typing) 40 14.00 -0.50 alignedtext
+468 219 moveto (Typing) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Typing -> Pretype_errors
-newpath 499 180 moveto
-510 180 522 180 534 180 curveto
+newpath 493 229 moveto
+510 236 534 246 554 254 curveto
 stroke
-newpath 534 178 moveto
-544 180 lineto
-534 183 lineto
+newpath 555 252 moveto
+563 258 lineto
+553 256 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Rawterm
 gsave 10 dict begin
-731 126 36 18 ellipse_path
+731 164 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-731 127 moveto (Rawterm) 51 14.00 -0.50 alignedtext
+731 165 moveto (Rawterm) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pretype_errors -> Rawterm
-newpath 630 166 moveto
-649 158 674 149 694 141 curveto
+newpath 630 258 moveto
+637 255 644 251 648 248 curveto
+667 233 692 206 710 187 curveto
 stroke
-newpath 692 139 moveto
-702 137 lineto
-694 144 lineto
+newpath 708 186 moveto
+716 180 lineto
+711 189 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Inductiveops
 gsave 10 dict begin
-731 180 46 18 ellipse_path
+731 245 46 18 ellipse_path
 stroke
 gsave 10 dict begin
-731 181 moveto (Inductiveops) 72 14.00 -0.50 alignedtext
+731 246 moveto (Inductiveops) 72 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pretype_errors -> Inductiveops
-newpath 648 180 moveto
-657 180 665 180 674 180 curveto
+newpath 641 263 moveto
+654 261 667 258 680 255 curveto
 stroke
-newpath 674 178 moveto
-684 180 lineto
-674 183 lineto
+newpath 679 253 moveto
+689 253 lineto
+680 258 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tacred
 gsave 10 dict begin
-731 34 29 18 ellipse_path
+731 56 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-731 35 moveto (Tacred) 38 14.00 -0.50 alignedtext
+731 57 moveto (Tacred) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Cbv
 gsave 10 dict begin
-863 46 27 18 ellipse_path
+863 56 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-863 47 moveto (Cbv) 23 14.00 -0.50 alignedtext
+863 57 moveto (Cbv) 23 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacred -> Cbv
-newpath 760 37 moveto
-780 39 806 41 827 43 curveto
+newpath 761 56 moveto
+781 56 806 56 827 56 curveto
 stroke
-newpath 826 40 moveto
-836 44 lineto
-826 45 lineto
+newpath 826 54 moveto
+836 56 lineto
+826 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Reductionops
 gsave 10 dict begin
-863 134 49 18 ellipse_path
+863 110 49 18 ellipse_path
 stroke
 gsave 10 dict begin
-863 135 moveto (Reductionops) 77 14.00 -0.50 alignedtext
+863 111 moveto (Reductionops) 77 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacred -> Reductionops
-newpath 752 47 moveto
-764 55 778 63 778 63 curveto
-795 75 819 96 837 111 curveto
+newpath 756 66 moveto
+774 74 800 84 821 92 curveto
 stroke
-newpath 838 109 moveto
-844 117 lineto
-835 112 lineto
+newpath 822 90 moveto
+830 96 lineto
+820 94 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Instantiate
 gsave 10 dict begin
-988 57 39 18 ellipse_path
+988 56 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-988 58 moveto (Instantiate) 58 14.00 -0.50 alignedtext
+988 57 moveto (Instantiate) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Cbv -> Instantiate
-newpath 890 48 moveto
-904 50 922 51 939 53 curveto
+newpath 890 56 moveto
+904 56 922 56 938 56 curveto
 stroke
-newpath 939 51 moveto
-949 54 lineto
-939 55 lineto
+newpath 938 54 moveto
+948 56 lineto
+938 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Reductionops -> Instantiate
-newpath 888 118 moveto
-908 106 936 89 957 77 curveto
+newpath 895 96 moveto
+912 88 933 80 951 72 curveto
 stroke
-newpath 954 76 moveto
-964 72 lineto
-957 80 lineto
+newpath 949 70 moveto
+959 68 lineto
+951 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Termops
 gsave 10 dict begin
-988 134 35 18 ellipse_path
+988 110 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-988 135 moveto (Termops) 49 14.00 -0.50 alignedtext
+988 111 moveto (Termops) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Reductionops -> Termops
-newpath 912 134 moveto
-923 134 933 134 943 134 curveto
+newpath 912 110 moveto
+923 110 933 110 943 110 curveto
 stroke
-newpath 943 132 moveto
-953 134 lineto
-943 137 lineto
+newpath 943 108 moveto
+953 110 lineto
+943 113 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Syntax_def
 gsave 10 dict begin
-596 126 42 18 ellipse_path
+596 164 42 18 ellipse_path
 stroke
 gsave 10 dict begin
-596 127 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
+596 165 moveto (Syntax_def) 63 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Syntax_def -> Rawterm
-newpath 638 126 moveto
-653 126 670 126 685 126 curveto
+newpath 638 164 moveto
+653 164 670 164 685 164 curveto
 stroke
-newpath 685 124 moveto
-695 126 lineto
-685 129 lineto
+newpath 685 162 moveto
+695 164 lineto
+685 167 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Retyping
 gsave 10 dict begin
-355 311 36 18 ellipse_path
+355 49 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-355 312 moveto (Retyping) 51 14.00 -0.50 alignedtext
+355 50 moveto (Retyping) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Retyping -> Reductionops
-newpath 388 318 moveto
-450 329 582 348 648 318 curveto
-713 288 802 199 842 157 curveto
-stroke
-newpath 839 157 moveto
-847 151 lineto
-843 160 lineto
+newpath 389 43 moveto
+469 30 670 2 778 26 curveto
+801 31 798 69 814 86 curveto
+817 89 820 91 824 92 curveto
+stroke
+newpath 825 90 moveto
+833 96 lineto
+823 94 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evd
 gsave 10 dict begin
-1091 57 27 18 ellipse_path
+1091 56 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1091 58 moveto (Evd) 22 14.00 -0.50 alignedtext
+1091 57 moveto (Evd) 22 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Instantiate -> Evd
-newpath 1028 57 moveto
-1037 57 1046 57 1054 57 curveto
+newpath 1028 56 moveto
+1037 56 1046 56 1054 56 curveto
 stroke
-newpath 1054 55 moveto
-1064 57 lineto
-1054 60 lineto
+newpath 1054 54 moveto
+1064 56 lineto
+1054 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Recordops
 gsave 10 dict begin
-468 72 40 18 ellipse_path
+468 110 40 18 ellipse_path
 stroke
 gsave 10 dict begin
-468 73 moveto (Recordops) 59 14.00 -0.50 alignedtext
+468 111 moveto (Recordops) 59 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Classops
 gsave 10 dict begin
-596 18 35 18 ellipse_path
+596 56 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-596 19 moveto (Classops) 49 14.00 -0.50 alignedtext
+596 57 moveto (Classops) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Recordops -> Classops
-newpath 497 60 moveto
-516 52 541 41 561 33 curveto
+newpath 497 98 moveto
+516 90 541 79 561 71 curveto
 stroke
-newpath 559 31 moveto
-569 30 lineto
-561 36 lineto
+newpath 559 69 moveto
+569 68 lineto
+561 74 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Classops -> Tacred
-newpath 630 22 moveto
-649 25 673 27 693 30 curveto
+newpath 631 56 moveto
+650 56 673 56 692 56 curveto
 stroke
-newpath 692 27 moveto
-702 31 lineto
-692 32 lineto
+newpath 691 54 moveto
+701 56 lineto
+691 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Classops -> Rawterm
-newpath 622 30 moveto
-635 36 648 42 648 42 curveto
-667 56 692 83 710 103 curveto
+newpath 622 68 moveto
+635 74 648 80 648 80 curveto
+667 94 692 121 710 141 curveto
 stroke
-newpath 711 100 moveto
-716 109 lineto
-707 104 lineto
+newpath 711 138 moveto
+716 147 lineto
+707 142 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pretyping
 gsave 10 dict begin
-46 245 37 18 ellipse_path
+46 114 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-46 246 moveto (Pretyping) 54 14.00 -0.50 alignedtext
+46 115 moveto (Pretyping) 54 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Cases
 gsave 10 dict begin
-147 245 27 18 ellipse_path
+147 114 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-147 246 moveto (Cases) 32 14.00 -0.50 alignedtext
+147 115 moveto (Cases) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pretyping -> Cases
-newpath 84 245 moveto
-93 245 102 245 110 245 curveto
+newpath 84 114 moveto
+93 114 102 114 110 114 curveto
 stroke
-newpath 110 243 moveto
-120 245 lineto
-110 248 lineto
+newpath 110 112 moveto
+120 114 lineto
+110 117 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coercion
 gsave 10 dict begin
-246 245 36 18 ellipse_path
+246 114 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-246 246 moveto (Coercion) 51 14.00 -0.50 alignedtext
+246 115 moveto (Coercion) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Cases -> Coercion
-newpath 174 245 moveto
-182 245 191 245 200 245 curveto
+newpath 174 114 moveto
+182 114 191 114 200 114 curveto
 stroke
-newpath 200 243 moveto
-210 245 lineto
-200 248 lineto
+newpath 200 112 moveto
+210 114 lineto
+200 117 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Inductiveops -> Reductionops
-newpath 766 168 moveto
-782 162 801 155 818 149 curveto
+newpath 748 228 moveto
+771 204 815 159 841 132 curveto
 stroke
-newpath 817 147 moveto
-827 146 lineto
-818 152 lineto
+newpath 837 132 moveto
+846 127 lineto
+841 136 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pattern
 gsave 10 dict begin
-596 72 30 18 ellipse_path
+596 110 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-596 73 moveto (Pattern) 39 14.00 -0.50 alignedtext
+596 111 moveto (Pattern) 39 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Pattern -> Reductionops
-newpath 626 75 moveto
-666 79 737 86 778 96 curveto
-785 98 806 107 826 117 curveto
+newpath 626 110 moveto
+670 110 751 110 806 110 curveto
 stroke
-newpath 825 114 moveto
-833 120 lineto
-823 118 lineto
+newpath 804 108 moveto
+814 110 lineto
+804 113 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pattern -> Rawterm
-newpath 621 82 moveto
-641 91 671 102 694 112 curveto
+newpath 621 120 moveto
+641 129 671 140 694 150 curveto
 stroke
-newpath 694 109 moveto
-703 115 lineto
-693 114 lineto
+newpath 694 147 moveto
+703 153 lineto
+693 152 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Indrec -> Inductiveops
-newpath 620 279 moveto
-631 274 642 269 648 264 curveto
-666 250 692 223 710 204 curveto
+newpath 619 316 moveto
+630 311 641 306 648 302 curveto
+663 293 683 279 700 267 curveto
 stroke
-newpath 708 203 moveto
-716 197 lineto
-711 206 lineto
+newpath 699 265 moveto
+708 261 lineto
+702 269 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -596,85 +596,82 @@ end grestore
 end grestore
 
 %	Evarconv -> Evarutil
-newpath 381 193 moveto
-397 201 418 211 435 218 curveto
+newpath 372 196 moveto
+388 212 412 235 428 248 curveto
+431 250 433 251 436 253 curveto
 stroke
-newpath 435 215 moveto
-443 222 lineto
-433 220 lineto
+newpath 438 251 moveto
+445 259 lineto
+435 256 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evarconv -> Typing
-newpath 392 180 moveto
-404 180 416 180 427 180 curveto
+newpath 386 190 moveto
+400 195 418 201 432 206 curveto
 stroke
-newpath 427 178 moveto
-437 180 lineto
-427 183 lineto
+newpath 432 203 moveto
+441 209 lineto
+431 208 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evarconv -> Recordops
-newpath 372 164 moveto
-391 145 422 116 444 95 curveto
+newpath 378 166 moveto
+395 156 418 141 436 130 curveto
 stroke
-newpath 442 93 moveto
-451 88 lineto
-446 97 lineto
+newpath 434 128 moveto
+444 125 lineto
+437 132 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Detyping
 gsave 10 dict begin
-596 234 36 18 ellipse_path
+596 218 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-596 235 moveto (Detyping) 52 14.00 -0.50 alignedtext
+596 219 moveto (Detyping) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Detyping -> Rawterm
-newpath 626 223 moveto
-634 220 643 215 648 210 curveto
-665 193 668 166 684 150 curveto
-684 150 689 147 697 144 curveto
-stroke
-newpath 696 142 moveto
-706 139 lineto
-698 146 lineto
+newpath 625 207 moveto
+645 199 673 188 694 179 curveto
+stroke
+newpath 693 177 moveto
+703 175 lineto
+695 181 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Detyping -> Termops
-newpath 632 230 moveto
-673 226 739 219 778 210 curveto
-825 199 868 180 912 164 curveto
-912 164 932 156 951 149 curveto
+%	Detyping -> Inductiveops
+newpath 630 225 moveto
+645 228 663 232 679 235 curveto
 stroke
-newpath 950 147 moveto
-960 145 lineto
-952 151 lineto
+newpath 680 233 moveto
+689 237 lineto
+679 237 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coercion -> Retyping
-newpath 269 259 moveto
-285 269 306 282 324 292 curveto
+newpath 269 100 moveto
+285 91 306 78 323 68 curveto
 stroke
-newpath 325 290 moveto
-332 297 lineto
-322 294 lineto
+newpath 321 66 moveto
+331 63 lineto
+324 70 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coercion -> Evarconv
-newpath 269 231 moveto
-285 222 306 209 323 199 curveto
+newpath 269 128 moveto
+285 138 306 151 324 161 curveto
 stroke
-newpath 321 197 moveto
-331 194 lineto
-324 201 lineto
+newpath 325 159 moveto
+332 166 lineto
+322 163 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index d05a3aba8..9679cb66f 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -431,22 +431,22 @@ newpath 502 117 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Errors
+%	Cerrors
 gsave 10 dict begin
-542 72 27 18 ellipse_path
+542 72 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 73 moveto (Errors) 34 14.00 -0.50 alignedtext
+542 73 moveto (Cerrors) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Protectedtoplevel -> Errors
+%	Protectedtoplevel -> Cerrors
 newpath 429 90 moveto
-455 86 484 81 507 78 curveto
+454 86 481 82 503 78 curveto
 stroke
-newpath 505 76 moveto
-515 77 lineto
-505 81 lineto
+newpath 502 76 moveto
+512 77 lineto
+502 81 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -470,9 +470,9 @@ newpath 488 32 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Errors -> Himsg
-newpath 570 73 moveto
-620 74 725 76 781 77 curveto
+%	Cerrors -> Himsg
+newpath 573 73 moveto
+625 74 726 76 782 77 curveto
 stroke
 newpath 779 75 moveto
 789 77 lineto