Mise a jour des dependances

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

7 files changed, 261 insertions, 253 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 3672e35d4..6b7d42d89 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 577 73
diff --git a/doc/library.dep.ps b/doc/library.dep.ps
index eb358f772..f79236717 100644
--- a/doc/library.dep.ps
+++ b/doc/library.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 543 235
diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps
index 9df862840..9a6de4273 100644
--- a/doc/parsing.dep.ps
+++ b/doc/parsing.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 576 232
diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps
index 8af063428..9246e91a5 100644
--- a/doc/pretyping.dep.ps
+++ b/doc/pretyping.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 577 203
diff --git a/doc/proofs.dep.ps b/doc/proofs.dep.ps
index 28297b5aa..29c50d955 100644
--- a/doc/proofs.dep.ps
+++ b/doc/proofs.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 124
+%%BoundingBox: 36 36 577 136
 %%EndComments
 %%BeginProlog
 save
@@ -150,205 +150,225 @@ def
 %%EndResource
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 124
+%%PageBoundingBox: 36 36 577 136
 %%PageOrientation: Portrait
 gsave
-35 35 542 89 boxprim clip newpath
+35 35 542 101 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.6067 set_scale
+0.6905 set_scale
 0 0 translate 0 rotate
-[ /CropBox [36 36 577 124] /PAGES pdfmark
+[ /CropBox [36 36 577 136] /PAGES pdfmark
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Tactic_debug
 gsave 10 dict begin
-167 126 48 18 ellipse_path
+167 18 48 18 ellipse_path
 stroke
 gsave 10 dict begin
-167 127 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
+167 19 moveto (Tactic_debug) 76 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacmach
 gsave 10 dict begin
-288 72 36 18 ellipse_path
+298 72 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-288 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
+298 73 moveto (Tacmach) 51 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tactic_debug -> Tacmach
-newpath 198 112 moveto
-215 104 235 95 252 88 curveto
+newpath 200 31 moveto
+219 39 243 49 262 57 curveto
 stroke
-newpath 251 86 moveto
-261 84 lineto
-253 90 lineto
+newpath 262 54 moveto
+270 60 lineto
+260 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evar_refiner
+%	Refiner
 gsave 10 dict begin
-406 72 45 18 ellipse_path
+411 99 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-406 73 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
+411 100 moveto (Refiner) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Tacmach -> Evar_refiner
-newpath 324 72 moveto
-332 72 341 72 350 72 curveto
+%	Tacmach -> Refiner
+newpath 331 80 moveto
+344 83 360 87 373 90 curveto
 stroke
-newpath 350 70 moveto
-360 72 lineto
-350 75 lineto
+newpath 373 87 moveto
+382 92 lineto
+372 92 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Refiner
+%	Logic
 gsave 10 dict begin
-519 72 31 18 ellipse_path
+505 99 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-519 73 moveto (Refiner) 41 14.00 -0.50 alignedtext
+505 100 moveto (Logic) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Evar_refiner -> Refiner
-newpath 452 72 moveto
-461 72 470 72 478 72 curveto
+%	Refiner -> Logic
+newpath 442 99 moveto
+450 99 459 99 468 99 curveto
 stroke
-newpath 478 70 moveto
-488 72 lineto
-478 75 lineto
+newpath 468 97 moveto
+478 99 lineto
+468 102 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tacinterp
 gsave 10 dict begin
-45 99 37 18 ellipse_path
+45 72 37 18 ellipse_path
 stroke
 gsave 10 dict begin
-45 100 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
+45 73 moveto (Tacinterp) 53 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacinterp -> Tactic_debug
-newpath 79 107 moveto
-90 109 103 112 115 115 curveto
+newpath 72 60 moveto
+88 53 109 44 127 36 curveto
 stroke
-newpath 116 113 moveto
-125 117 lineto
-115 117 lineto
+newpath 126 34 moveto
+136 32 lineto
+128 38 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pfedit
 gsave 10 dict begin
-167 72 27 18 ellipse_path
+167 126 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-167 73 moveto (Pfedit) 33 14.00 -0.50 alignedtext
+167 127 moveto (Pfedit) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacinterp -> Pfedit
-newpath 79 91 moveto
-96 88 116 83 132 80 curveto
+newpath 72 84 moveto
+91 93 117 104 136 112 curveto
 stroke
-newpath 131 78 moveto
-141 78 lineto
-132 83 lineto
+newpath 136 109 moveto
+144 116 lineto
+134 114 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Pfedit -> Tacmach
-newpath 194 72 moveto
-208 72 226 72 242 72 curveto
+newpath 190 116 moveto
+210 108 239 96 261 87 curveto
 stroke
-newpath 242 70 moveto
-252 72 lineto
-242 75 lineto
+newpath 260 85 moveto
+270 83 lineto
+262 89 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Logic
+%	Evar_refiner
 gsave 10 dict begin
-613 72 27 18 ellipse_path
+298 126 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-613 73 moveto (Logic) 32 14.00 -0.50 alignedtext
+298 127 moveto (Evar_refiner) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Refiner -> Logic
-newpath 550 72 moveto
-558 72 567 72 576 72 curveto
+%	Pfedit -> Evar_refiner
+newpath 194 126 moveto
+208 126 226 126 242 126 curveto
 stroke
-newpath 576 70 moveto
-586 72 lineto
-576 75 lineto
+newpath 242 124 moveto
+252 126 lineto
+242 129 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Proof_trees
 gsave 10 dict begin
-719 72 42 18 ellipse_path
+611 99 42 18 ellipse_path
 stroke
 gsave 10 dict begin
-719 73 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
+611 100 moveto (Proof_trees) 64 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Logic -> Proof_trees
-newpath 640 72 moveto
-648 72 657 72 666 72 curveto
+newpath 532 99 moveto
+540 99 549 99 558 99 curveto
 stroke
-newpath 666 70 moveto
-676 72 lineto
-666 75 lineto
+newpath 558 97 moveto
+568 99 lineto
+558 102 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Proof_type
 gsave 10 dict begin
-840 72 41 18 ellipse_path
+732 99 41 18 ellipse_path
 stroke
 gsave 10 dict begin
-840 73 moveto (Proof_type) 62 14.00 -0.50 alignedtext
+732 100 moveto (Proof_type) 62 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Proof_trees -> Proof_type
-newpath 762 72 moveto
-771 72 780 72 788 72 curveto
+newpath 654 99 moveto
+663 99 672 99 680 99 curveto
 stroke
-newpath 788 70 moveto
-798 72 lineto
-788 75 lineto
+newpath 680 97 moveto
+690 99 lineto
+680 102 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Evar_refiner -> Refiner
+newpath 337 117 moveto
+349 114 362 111 373 108 curveto
+stroke
+newpath 372 106 moveto
+382 106 lineto
+373 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Clenv
 gsave 10 dict begin
-167 18 27 18 ellipse_path
+167 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-167 19 moveto (Clenv) 33 14.00 -0.50 alignedtext
+167 73 moveto (Clenv) 33 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Clenv -> Tacmach
-newpath 189 28 moveto
-206 36 232 48 252 56 curveto
+newpath 194 72 moveto
+211 72 232 72 252 72 curveto
+stroke
+newpath 252 70 moveto
+262 72 lineto
+252 75 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Clenv -> Evar_refiner
+newpath 190 82 moveto
+208 89 235 100 257 109 curveto
 stroke
-newpath 253 54 moveto
-261 60 lineto
-251 58 lineto
+newpath 258 107 moveto
+266 113 lineto
+256 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage
diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index a628a56d9..0ec3a8272 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 577 125
diff --git a/doc/toplevel.dep.ps b/doc/toplevel.dep.ps
index 725910c85..44a92446d 100644
--- a/doc/toplevel.dep.ps
+++ b/doc/toplevel.dep.ps
@@ -1,6 +1,6 @@
 %!PS-Adobe-2.0
 %%Creator: dot version gviz 1.7.3b (Mon Feb 26 14:10:22 EST 2001)
-%%For: (herbelin) Hugo Herbelin
+%%For: (clrenard) Clement Renard
 %%Title: G
 %%Pages: (atend)
 %%BoundingBox: 36 36 576 256
@@ -164,416 +164,404 @@ gsave
 
 %	Vernac
 gsave 10 dict begin
-542 226 30 18 ellipse_path
+542 126 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 227 moveto (Vernac) 40 14.00 -0.50 alignedtext
+542 127 moveto (Vernac) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp
 gsave 10 dict begin
-695 234 46 18 ellipse_path
+695 118 46 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 235 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
+695 119 moveto (Vernacinterp) 72 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernac -> Vernacinterp
-newpath 573 228 moveto
-592 229 619 230 642 231 curveto
+newpath 573 124 moveto
+592 123 619 122 642 121 curveto
 stroke
-newpath 639 228 moveto
-649 232 lineto
-639 233 lineto
+newpath 639 119 moveto
+649 120 lineto
+639 124 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Command
 gsave 10 dict begin
-818 203 39 18 ellipse_path
+818 155 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 204 moveto (Command) 58 14.00 -0.50 alignedtext
+818 156 moveto (Command) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp -> Command
-newpath 734 224 moveto
-747 221 761 218 774 214 curveto
+newpath 732 129 moveto
+746 133 761 138 776 142 curveto
 stroke
-newpath 773 212 moveto
-783 212 lineto
-774 217 lineto
+newpath 776 139 moveto
+785 145 lineto
+775 144 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Himsg
 gsave 10 dict begin
-818 257 29 18 ellipse_path
+818 78 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 258 moveto (Himsg) 37 14.00 -0.50 alignedtext
+818 79 moveto (Himsg) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacinterp -> Himsg
-newpath 737 242 moveto
-752 244 767 248 781 250 curveto
+newpath 731 106 moveto
+748 101 768 94 784 89 curveto
 stroke
-newpath 781 247 moveto
-790 252 lineto
-780 252 lineto
+newpath 782 87 moveto
+792 86 lineto
+784 92 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Vernacentries
 gsave 10 dict begin
-542 126 49 18 ellipse_path
+542 226 49 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 127 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
+542 227 moveto (Vernacentries) 77 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Vernacinterp
-newpath 562 143 moveto
-586 162 624 193 648 210 curveto
-651 212 655 215 660 217 curveto
+newpath 562 209 moveto
+586 190 624 159 648 142 curveto
+651 140 655 137 660 135 curveto
 stroke
-newpath 658 213 moveto
-666 220 lineto
-656 218 lineto
+newpath 656 134 moveto
+666 132 lineto
+658 139 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Discharge
 gsave 10 dict begin
-695 126 38 18 ellipse_path
+695 280 38 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 127 moveto (Discharge) 56 14.00 -0.50 alignedtext
+695 281 moveto (Discharge) 56 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Discharge
-newpath 591 126 moveto
-609 126 629 126 647 126 curveto
+newpath 577 239 moveto
+601 247 631 257 656 266 curveto
 stroke
-newpath 646 124 moveto
-656 126 lineto
-646 129 lineto
+newpath 656 263 moveto
+664 269 lineto
+654 268 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Metasyntax
 gsave 10 dict begin
-695 72 43 18 ellipse_path
+695 226 43 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 73 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
+695 227 moveto (Metasyntax) 65 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Metasyntax
-newpath 577 113 moveto
-600 106 630 96 653 87 curveto
+newpath 591 226 moveto
+608 226 626 226 642 226 curveto
 stroke
-newpath 652 85 moveto
-662 84 lineto
-653 90 lineto
+newpath 642 224 moveto
+652 226 lineto
+642 229 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Mltop
 gsave 10 dict begin
-695 18 27 18 ellipse_path
+695 334 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 19 moveto (Mltop) 34 14.00 -0.50 alignedtext
+695 335 moveto (Mltop) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Mltop
-newpath 562 109 moveto
-586 90 624 59 648 42 curveto
-653 39 659 35 666 32 curveto
+newpath 562 243 moveto
+586 262 624 293 648 310 curveto
+653 313 659 317 666 320 curveto
 stroke
-newpath 662 31 moveto
-672 29 lineto
-664 36 lineto
+newpath 664 316 moveto
+672 323 lineto
+662 321 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Record
 gsave 10 dict begin
-695 180 30 18 ellipse_path
+695 172 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-695 181 moveto (Record) 40 14.00 -0.50 alignedtext
+695 173 moveto (Record) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Vernacentries -> Record
-newpath 577 139 moveto
-602 147 636 159 661 168 curveto
+newpath 577 213 moveto
+602 205 636 193 661 184 curveto
 stroke
-newpath 661 165 moveto
-669 171 lineto
-659 170 lineto
+newpath 659 182 moveto
+669 181 lineto
+661 187 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Class
 gsave 10 dict begin
-818 149 27 18 ellipse_path
+818 220 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 150 moveto (Class) 30 14.00 -0.50 alignedtext
+818 221 moveto (Class) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Discharge -> Class
-newpath 731 133 moveto
-747 136 766 140 783 142 curveto
+newpath 722 267 moveto
+741 257 768 245 788 235 curveto
 stroke
-newpath 783 139 moveto
-792 144 lineto
-782 144 lineto
+newpath 786 233 moveto
+796 231 lineto
+788 238 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Recordobj
 gsave 10 dict begin
-818 95 39 18 ellipse_path
+818 280 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-818 96 moveto (Recordobj) 58 14.00 -0.50 alignedtext
+818 281 moveto (Recordobj) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Discharge -> Recordobj
-newpath 729 117 moveto
-743 114 759 110 774 106 curveto
+newpath 734 280 moveto
+745 280 757 280 768 280 curveto
 stroke
-newpath 773 104 moveto
-783 104 lineto
-774 109 lineto
+newpath 768 278 moveto
+778 280 lineto
+768 283 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Record -> Command
-newpath 724 185 moveto
-738 187 756 191 771 194 curveto
+newpath 725 168 moveto
+738 166 755 164 770 162 curveto
 stroke
-newpath 772 192 moveto
-781 196 lineto
-771 196 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Record -> Himsg
-newpath 718 192 moveto
-730 198 742 204 742 204 curveto
-755 212 766 224 778 233 curveto
-781 235 786 238 791 240 curveto
-stroke
-newpath 790 236 moveto
-797 244 lineto
-787 241 lineto
+newpath 770 160 moveto
+780 160 lineto
+771 164 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Record -> Class
-newpath 723 173 moveto
-741 169 764 163 784 158 curveto
+newpath 720 182 moveto
+739 189 765 199 786 207 curveto
 stroke
-newpath 783 156 moveto
-793 156 lineto
-784 161 lineto
+newpath 786 204 moveto
+794 211 lineto
+784 209 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Toplevel
 gsave 10 dict begin
-247 122 35 18 ellipse_path
+247 199 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-247 123 moveto (Toplevel) 49 14.00 -0.50 alignedtext
+247 200 moveto (Toplevel) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Mltop
-newpath 279 115 moveto
-361 96 578 45 662 26 curveto
+newpath 277 208 moveto
+359 233 579 299 663 324 curveto
 stroke
-newpath 659 24 moveto
-669 24 lineto
-660 29 lineto
+newpath 661 321 moveto
+670 326 lineto
+660 326 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel
 gsave 10 dict begin
-377 253 59 18 ellipse_path
+377 99 59 18 ellipse_path
 stroke
 gsave 10 dict begin
-377 254 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
+377 100 moveto (Protectedtoplevel) 97 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Toplevel -> Protectedtoplevel
-newpath 263 138 moveto
-286 161 328 204 355 231 curveto
+newpath 266 184 moveto
+288 168 322 141 347 122 curveto
 stroke
-newpath 355 227 moveto
-360 236 lineto
-351 231 lineto
+newpath 346 120 moveto
+355 116 lineto
+349 124 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Protectedtoplevel -> Vernac
-newpath 429 244 moveto
-454 240 481 236 503 232 curveto
+newpath 429 108 moveto
+454 112 481 116 503 120 curveto
 stroke
-newpath 502 230 moveto
-512 231 lineto
-502 235 lineto
+newpath 502 117 moveto
+512 121 lineto
+502 122 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Errors
 gsave 10 dict begin
-542 280 27 18 ellipse_path
+542 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 281 moveto (Errors) 34 14.00 -0.50 alignedtext
+542 73 moveto (Errors) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Protectedtoplevel -> Errors
-newpath 429 262 moveto
-455 266 484 271 507 274 curveto
+newpath 429 90 moveto
+455 86 484 81 507 78 curveto
 stroke
-newpath 505 271 moveto
-515 275 lineto
-505 276 lineto
+newpath 505 76 moveto
+515 77 lineto
+505 81 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Line_oriented_parser
 gsave 10 dict begin
-542 334 70 18 ellipse_path
+542 18 70 18 ellipse_path
 stroke
 gsave 10 dict begin
-542 335 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
+542 19 moveto (Line_oriented_parser) 119 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Protectedtoplevel -> Line_oriented_parser
-newpath 403 269 moveto
-424 282 453 300 472 310 curveto
-477 312 484 315 491 318 curveto
+newpath 403 83 moveto
+424 70 453 52 472 42 curveto
+477 40 484 37 491 34 curveto
 stroke
-newpath 489 315 moveto
-498 320 lineto
-488 320 lineto
+newpath 488 32 moveto
+498 32 lineto
+489 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Errors -> Himsg
-newpath 569 278 moveto
-619 274 725 265 781 260 curveto
+newpath 570 73 moveto
+620 74 725 76 781 77 curveto
 stroke
-newpath 779 258 moveto
-789 259 lineto
-779 263 lineto
+newpath 779 75 moveto
+789 77 lineto
+779 80 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Minicoq
 gsave 10 dict begin
-42 230 34 18 ellipse_path
+42 253 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-42 231 moveto (Minicoq) 47 14.00 -0.50 alignedtext
+42 254 moveto (Minicoq) 47 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Fhimsg
 gsave 10 dict begin
-144 230 31 18 ellipse_path
+144 253 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-144 231 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
+144 254 moveto (Fhimsg) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Minicoq -> Fhimsg
-newpath 76 230 moveto
-85 230 94 230 102 230 curveto
+newpath 76 253 moveto
+85 253 94 253 102 253 curveto
 stroke
-newpath 102 228 moveto
-112 230 lineto
-102 233 lineto
+newpath 102 251 moveto
+112 253 lineto
+102 256 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqtop
 gsave 10 dict begin
-42 149 31 18 ellipse_path
+42 172 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-42 150 moveto (Coqtop) 41 14.00 -0.50 alignedtext
+42 173 moveto (Coqtop) 41 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqinit
 gsave 10 dict begin
-144 122 31 18 ellipse_path
+144 199 31 18 ellipse_path
 stroke
 gsave 10 dict begin
-144 123 moveto (Coqinit) 42 14.00 -0.50 alignedtext
+144 200 moveto (Coqinit) 42 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqtop -> Coqinit
-newpath 70 141 moveto
-81 138 94 135 106 132 curveto
+newpath 70 180 moveto
+81 183 94 186 106 189 curveto
 stroke
-newpath 105 130 moveto
-115 129 lineto
-106 135 lineto
+newpath 106 186 moveto
+115 192 lineto
+105 191 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Usage
 gsave 10 dict begin
-144 176 27 18 ellipse_path
+144 145 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-144 177 moveto (Usage) 34 14.00 -0.50 alignedtext
+144 146 moveto (Usage) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Coqtop -> Usage
-newpath 70 157 moveto
-82 160 96 164 109 167 curveto
+newpath 70 164 moveto
+82 161 96 157 109 154 curveto
 stroke
-newpath 109 164 moveto
-118 169 lineto
-108 169 lineto
+newpath 108 152 moveto
+118 152 lineto
+109 157 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Coqinit -> Toplevel
-newpath 176 122 moveto
-184 122 193 122 202 122 curveto
+newpath 176 199 moveto
+184 199 193 199 202 199 curveto
 stroke
-newpath 202 120 moveto
-212 122 lineto
-202 125 lineto
+newpath 202 197 moveto
+212 199 lineto
+202 202 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage