mise a jour

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

1 files changed, 225 insertions, 194 deletions

diff --git a/doc/tactics.dep.ps b/doc/tactics.dep.ps
index 940e81966..5e8125d5e 100644
--- a/doc/tactics.dep.ps
+++ b/doc/tactics.dep.ps
@@ -1,9 +1,9 @@
 %!PS-Adobe-2.0
 %%Creator: dot version uwin98 (01-26-98)
-%%For: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 194
+%%BoundingBox: 36 36 577 193
 %%EndComments
 %%BeginProlog
 save
@@ -47,7 +47,7 @@ DotDict begin
 		gsave
 			coordfont setfont
 			0 0 moveto
-			(\() show i str cvs show (,) show j str cvs show (\)) show
+			(() show i str cvs show (,) show j str cvs show ()) show
 		grestore
 	} if
 } bind def
@@ -139,396 +139,427 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 194
+%%PageBoundingBox: 36 36 577 193
 gsave
-35 35 542 159 boxprim clip newpath
+35 35 542 158 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.6618 set_scale
+0.6250 set_scale
 0 0 translate 0 rotate
 0.000 0.000 0.000 graphcolor
 14.00 /Times-Roman set_font
 
 %	Termdn
 gsave 10 dict begin
-653 202 32 18 ellipse_path
+701 233 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-653 203 moveto (Termdn) 44 14.00 -0.50 alignedtext
+701 234 moveto (Termdn) 44 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Dn
 gsave 10 dict begin
-771 202 27 18 ellipse_path
+819 233 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-771 203 moveto (Dn) 17 14.00 -0.50 alignedtext
+819 234 moveto (Dn) 17 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Termdn -> Dn
-newpath 686 202 moveto
-701 202 719 202 735 202 curveto
+newpath 734 233 moveto
+749 233 767 233 783 233 curveto
 stroke
-newpath 734 200 moveto
-744 202 lineto
-734 205 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Tauto
-gsave 10 dict begin
-127 220 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-127 221 moveto (Tauto) 32 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Auto
-gsave 10 dict begin
-217 166 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-217 167 moveto (Auto) 28 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Tauto -> Auto
-newpath 147 208 moveto
-159 201 175 191 189 183 curveto
-stroke
-newpath 187 181 moveto
-197 178 lineto
-190 185 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Hiddentac
-gsave 10 dict begin
-319 114 39 18 ellipse_path
-stroke
-gsave 10 dict begin
-319 115 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Auto -> Hiddentac
-newpath 239 155 moveto
-252 148 269 140 284 132 curveto
-stroke
-newpath 283 130 moveto
-293 128 lineto
-285 134 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Dhyp
-gsave 10 dict begin
-319 168 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-319 169 moveto (Dhyp) 31 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Auto -> Dhyp
-newpath 244 167 moveto
-256 167 270 167 282 167 curveto
-stroke
-newpath 282 165 moveto
-292 167 lineto
-282 170 lineto
+newpath 782 231 moveto
+792 233 lineto
+782 236 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tactics
 gsave 10 dict begin
-545 87 30 18 ellipse_path
+593 110 30 18 ellipse_path
 stroke
 gsave 10 dict begin
-545 88 moveto (Tactics) 40 14.00 -0.50 alignedtext
+593 111 moveto (Tactics) 40 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Hipattern
 gsave 10 dict begin
-653 114 36 18 ellipse_path
+701 156 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-653 115 moveto (Hipattern) 52 14.00 -0.50 alignedtext
+701 157 moveto (Hipattern) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tactics -> Hipattern
-newpath 573 94 moveto
-584 97 598 100 610 104 curveto
+newpath 618 121 moveto
+631 127 649 134 664 140 curveto
 stroke
-newpath 611 102 moveto
-620 106 lineto
-610 106 lineto
+newpath 665 138 moveto
+673 144 lineto
+663 142 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tacticals
 gsave 10 dict begin
-653 60 35 18 ellipse_path
+701 102 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-653 61 moveto (Tacticals) 50 14.00 -0.50 alignedtext
+701 103 moveto (Tacticals) 50 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tactics -> Tacticals
-newpath 573 80 moveto
-585 77 599 74 612 70 curveto
+newpath 623 108 moveto
+633 107 645 106 656 105 curveto
 stroke
-newpath 611 68 moveto
-621 68 lineto
-612 73 lineto
+newpath 656 103 moveto
+666 104 lineto
+656 107 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Wcclausenv
 gsave 10 dict begin
-771 60 44 18 ellipse_path
+819 102 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-771 61 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
+819 103 moveto (Wcclausenv) 68 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacticals -> Wcclausenv
-newpath 689 60 moveto
-698 60 707 60 716 60 curveto
+newpath 737 102 moveto
+746 102 755 102 764 102 curveto
 stroke
-newpath 716 58 moveto
-726 60 lineto
-716 63 lineto
+newpath 764 100 moveto
+774 102 lineto
+764 105 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Tacentries
 gsave 10 dict begin
-434 110 39 18 ellipse_path
+482 141 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-434 111 moveto (Tacentries) 58 14.00 -0.50 alignedtext
+482 142 moveto (Tacentries) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Tacentries -> Tactics
-newpath 470 103 moveto
-482 101 495 98 507 95 curveto
+newpath 516 132 moveto
+529 128 543 124 556 120 curveto
 stroke
-newpath 506 93 moveto
-516 93 lineto
-507 98 lineto
+newpath 555 118 moveto
+565 118 lineto
+556 123 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Refine
 gsave 10 dict begin
-434 18 29 18 ellipse_path
+482 87 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-434 19 moveto (Refine) 37 14.00 -0.50 alignedtext
+482 88 moveto (Refine) 37 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Refine -> Tactics
-newpath 455 31 moveto
-473 42 497 57 516 69 curveto
+newpath 510 93 moveto
+523 95 540 99 554 102 curveto
 stroke
-newpath 517 67 moveto
-524 74 lineto
-514 71 lineto
+newpath 555 100 moveto
+564 104 lineto
+554 104 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Nbtermdn
 gsave 10 dict begin
-434 202 38 18 ellipse_path
+482 233 38 18 ellipse_path
 stroke
 gsave 10 dict begin
-434 203 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
+482 234 moveto (Nbtermdn) 56 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Btermdn
 gsave 10 dict begin
-545 202 35 18 ellipse_path
+593 233 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-545 203 moveto (Btermdn) 49 14.00 -0.50 alignedtext
+593 234 moveto (Btermdn) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Nbtermdn -> Btermdn
-newpath 473 202 moveto
-482 202 491 202 500 202 curveto
+newpath 521 233 moveto
+530 233 539 233 548 233 curveto
 stroke
-newpath 500 200 moveto
-510 202 lineto
-500 205 lineto
+newpath 548 231 moveto
+558 233 lineto
+548 236 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Btermdn -> Termdn
-newpath 580 202 moveto
-590 202 601 202 611 202 curveto
+newpath 628 233 moveto
+638 233 649 233 659 233 curveto
 stroke
-newpath 610 200 moveto
-620 202 lineto
-610 205 lineto
+newpath 658 231 moveto
+668 233 lineto
+658 236 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Leminv
 gsave 10 dict begin
-32 112 32 18 ellipse_path
+32 126 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-32 113 moveto (Leminv) 43 14.00 -0.50 alignedtext
+32 127 moveto (Leminv) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Inv
 gsave 10 dict begin
-127 112 27 18 ellipse_path
+144 126 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-127 113 moveto (Inv) 18 14.00 -0.50 alignedtext
+144 127 moveto (Inv) 18 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Leminv -> Inv
-newpath 64 112 moveto
-73 112 82 112 90 112 curveto
+newpath 64 126 moveto
+78 126 94 126 108 126 curveto
 stroke
-newpath 90 110 moveto
-100 112 lineto
-90 115 lineto
+newpath 107 124 moveto
+117 126 lineto
+107 129 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
+%	Auto
+gsave 10 dict begin
+258 180 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+258 181 moveto (Auto) 28 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
 %	Inv -> Auto
-newpath 147 124 moveto
-159 131 175 141 189 149 curveto
+newpath 166 137 moveto
+183 145 208 156 227 165 curveto
 stroke
-newpath 190 147 moveto
-197 154 lineto
-187 151 lineto
+newpath 228 163 moveto
+236 169 lineto
+226 167 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Elim
 gsave 10 dict begin
-217 112 27 18 ellipse_path
+258 126 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-217 113 moveto (Elim) 27 14.00 -0.50 alignedtext
+258 127 moveto (Elim) 27 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Inv -> Elim
-newpath 154 112 moveto
-162 112 171 112 180 112 curveto
+newpath 171 126 moveto
+186 126 205 126 222 126 curveto
 stroke
-newpath 180 110 moveto
-190 112 lineto
-180 115 lineto
+newpath 221 124 moveto
+231 126 lineto
+221 129 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Equality
 gsave 10 dict begin
-319 60 34 18 ellipse_path
+258 62 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-319 61 moveto (Equality) 47 14.00 -0.50 alignedtext
+258 63 moveto (Equality) 47 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Inv -> Equality
-newpath 148 101 moveto
-161 93 178 85 190 82 curveto
-213 76 249 69 277 65 curveto
+newpath 165 114 moveto
+183 104 207 91 227 80 curveto
 stroke
-newpath 276 63 moveto
-286 64 lineto
-276 68 lineto
+newpath 225 78 moveto
+235 75 lineto
+228 82 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Hiddentac
+gsave 10 dict begin
+367 137 39 18 ellipse_path
+stroke
+gsave 10 dict begin
+367 138 moveto (Hiddentac) 57 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Auto -> Hiddentac
+newpath 281 171 moveto
+294 165 313 159 328 153 curveto
+stroke
+newpath 327 151 moveto
+337 149 lineto
+329 155 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Dhyp
+gsave 10 dict begin
+367 191 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+367 192 moveto (Dhyp) 31 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Auto -> Dhyp
+newpath 285 183 moveto
+299 185 316 186 330 187 curveto
+stroke
+newpath 330 185 moveto
+340 188 lineto
+330 189 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Elim -> Hiddentac
-newpath 244 113 moveto
-252 113 261 113 270 113 curveto
+newpath 285 129 moveto
+295 130 307 131 319 132 curveto
 stroke
-newpath 270 111 moveto
-280 113 lineto
-270 116 lineto
+newpath 319 130 moveto
+329 133 lineto
+319 134 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Equality -> Tactics
-newpath 352 64 moveto
-393 69 463 77 506 82 curveto
+newpath 291 57 moveto
+347 48 461 36 522 57 curveto
+536 62 555 76 569 89 curveto
 stroke
-newpath 505 79 moveto
-515 83 lineto
-505 84 lineto
+newpath 570 87 moveto
+576 95 lineto
+567 90 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Hiddentac -> Tacentries
-newpath 358 113 moveto
-367 112 375 112 384 112 curveto
+newpath 406 138 moveto
+415 139 423 139 432 139 curveto
 stroke
-newpath 384 110 moveto
-394 111 lineto
-384 114 lineto
+newpath 432 137 moveto
+442 140 lineto
+432 141 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Eqdecide
+gsave 10 dict begin
+144 72 36 18 ellipse_path
+stroke
+gsave 10 dict begin
+144 73 moveto (Eqdecide) 51 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Eqdecide -> Auto
+newpath 171 84 moveto
+178 88 184 92 188 96 curveto
+205 113 210 139 224 156 curveto
+225 158 227 160 229 162 curveto
+stroke
+newpath 231 160 moveto
+238 168 lineto
+228 165 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Eqdecide -> Equality
+newpath 180 69 moveto
+191 68 203 67 214 66 curveto
+stroke
+newpath 214 64 moveto
+224 65 lineto
+214 68 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Eauto
 gsave 10 dict begin
-127 166 27 18 ellipse_path
+144 180 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-127 167 moveto (Eauto) 32 14.00 -0.50 alignedtext
+144 181 moveto (Eauto) 32 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Eauto -> Auto
-newpath 154 166 moveto
-162 166 171 166 180 166 curveto
+newpath 171 180 moveto
+186 180 205 180 222 180 curveto
 stroke
-newpath 180 164 moveto
-190 166 lineto
-180 169 lineto
+newpath 221 178 moveto
+231 180 lineto
+221 183 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Dhyp -> Tactics
-newpath 346 165 moveto
-380 160 441 152 474 140 curveto
-488 135 507 121 521 108 curveto
+newpath 394 190 moveto
+429 188 489 183 522 171 curveto
+538 166 558 148 573 133 curveto
 stroke
-newpath 519 107 moveto
-528 102 lineto
-522 110 lineto
+newpath 571 132 moveto
+579 126 lineto
+574 135 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Dhyp -> Nbtermdn
-newpath 344 175 moveto
-358 179 376 185 392 189 curveto
+newpath 391 200 moveto
+406 205 426 212 442 219 curveto
+stroke
+newpath 442 216 moveto
+451 222 lineto
+441 221 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Autorewrite
+gsave 10 dict begin
+144 18 44 18 ellipse_path
+stroke
+gsave 10 dict begin
+144 19 moveto (Autorewrite) 67 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Autorewrite -> Equality
+newpath 176 30 moveto
+190 36 207 42 222 48 curveto
 stroke
-newpath 392 186 moveto
-401 192 lineto
-391 191 lineto
+newpath 222 45 moveto
+231 51 lineto
+221 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage