mise a jour

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

1 files changed, 139 insertions, 109 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 692a28e87c..3604e5ea61 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -3,7 +3,7 @@
 %%For: Gros nain
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 576 73
+%%BoundingBox: 36 36 576 91
 %%EndComments
 %%BeginProlog
 save
@@ -139,9 +139,9 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 576 73
+%%PageBoundingBox: 36 36 576 91
 gsave
-35 35 541 38 boxprim clip newpath
+35 35 541 56 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
 0.3994 set_scale
@@ -151,38 +151,38 @@ gsave
 
 %	Univ
 gsave 10 dict begin
-1229 47 27 18 ellipse_path
+1229 74 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1229 48 moveto (Univ) 28 14.00 -0.50 alignedtext
+1229 75 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1322 47 29 18 ellipse_path
+1322 74 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1322 48 moveto (Names) 38 14.00 -0.50 alignedtext
+1322 75 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1256 47 moveto
-1264 47 1273 47 1282 47 curveto
+newpath 1256 74 moveto
+1264 74 1273 74 1282 74 curveto
 stroke
-newpath 1282 45 moveto
-1292 47 lineto
-1282 50 lineto
+newpath 1282 72 moveto
+1292 74 lineto
+1282 77 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Typeops
 gsave 10 dict begin
-265 45 34 18 ellipse_path
+265 64 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-265 46 moveto (Typeops) 48 14.00 -0.50 alignedtext
+265 65 moveto (Typeops) 48 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
@@ -196,12 +196,12 @@ end grestore
 end grestore
 
 %	Typeops -> Inductive
-newpath 297 52 moveto
-310 55 325 58 339 62 curveto
+newpath 299 66 moveto
+310 67 323 68 334 69 curveto
 stroke
-newpath 339 59 moveto
-348 64 lineto
-338 64 lineto
+newpath 334 67 moveto
+344 70 lineto
+334 71 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -215,232 +215,262 @@ end grestore
 end grestore
 
 %	Typeops -> Type_errors
-newpath 297 38 moveto
-308 36 321 33 333 30 curveto
+newpath 292 53 moveto
+306 47 324 41 340 35 curveto
 stroke
-newpath 332 28 moveto
-342 27 lineto
-333 33 lineto
+newpath 339 33 moveto
+349 31 lineto
+341 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Reduction
 gsave 10 dict begin
-501 45 39 18 ellipse_path
+501 72 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-501 46 moveto (Reduction) 57 14.00 -0.50 alignedtext
+501 73 moveto (Reduction) 57 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Inductive -> Reduction
-newpath 414 64 moveto
-427 61 442 58 456 55 curveto
+newpath 418 72 moveto
+429 72 441 72 452 72 curveto
 stroke
-newpath 456 53 moveto
-466 53 lineto
-457 57 lineto
+newpath 452 70 moveto
+462 72 lineto
+452 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Type_errors -> Reduction
-newpath 420 27 moveto
-432 29 444 32 456 35 curveto
+newpath 411 31 moveto
+427 39 448 48 465 55 curveto
 stroke
-newpath 456 32 moveto
-465 37 lineto
-455 37 lineto
+newpath 465 52 moveto
+473 59 lineto
+463 57 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Closure
 gsave 10 dict begin
-608 45 32 18 ellipse_path
+608 72 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-608 46 moveto (Closure) 43 14.00 -0.50 alignedtext
+608 73 moveto (Closure) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Reduction -> Closure
-newpath 540 45 moveto
-549 45 558 45 566 45 curveto
+newpath 540 72 moveto
+549 72 558 72 566 72 curveto
 stroke
-newpath 566 43 moveto
-576 45 lineto
-566 48 lineto
+newpath 566 70 moveto
+576 72 lineto
+566 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Term
 gsave 10 dict begin
-1139 47 27 18 ellipse_path
+1139 74 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1139 48 moveto (Term) 30 14.00 -0.50 alignedtext
+1139 75 moveto (Term) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Univ
-newpath 1166 47 moveto
-1174 47 1183 47 1192 47 curveto
+newpath 1166 74 moveto
+1174 74 1183 74 1192 74 curveto
 stroke
-newpath 1192 45 moveto
-1202 47 lineto
-1192 50 lineto
+newpath 1192 72 moveto
+1202 74 lineto
+1192 77 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sign
 gsave 10 dict begin
-1049 47 27 18 ellipse_path
+1049 74 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1049 48 moveto (Sign) 25 14.00 -0.50 alignedtext
+1049 75 moveto (Sign) 25 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sign -> Term
-newpath 1076 47 moveto
-1084 47 1093 47 1102 47 curveto
+newpath 1076 74 moveto
+1084 74 1093 74 1102 74 curveto
 stroke
-newpath 1102 45 moveto
-1112 47 lineto
-1102 50 lineto
+newpath 1102 72 moveto
+1112 74 lineto
+1102 77 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Safe_typing
 gsave 10 dict begin
-44 45 44 18 ellipse_path
+44 92 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-44 46 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
+44 93 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
+%	Cooking
+gsave 10 dict begin
+265 118 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+265 119 moveto (Cooking) 48 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Safe_typing -> Cooking
+newpath 86 97 moveto
+126 102 184 109 223 113 curveto
+stroke
+newpath 221 110 moveto
+231 114 lineto
+221 115 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
 %	Indtypes
 gsave 10 dict begin
-159 45 34 18 ellipse_path
+159 68 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-159 46 moveto (Indtypes) 48 14.00 -0.50 alignedtext
+159 69 moveto (Indtypes) 48 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Safe_typing -> Indtypes
-newpath 88 45 moveto
-97 45 106 45 114 45 curveto
+newpath 83 84 moveto
+94 82 106 79 117 77 curveto
+stroke
+newpath 117 75 moveto
+127 75 lineto
+118 79 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Cooking -> Reduction
+newpath 300 116 moveto
+336 113 393 108 426 102 curveto
+426 102 444 95 462 87 curveto
 stroke
-newpath 114 43 moveto
-124 45 lineto
-114 48 lineto
+newpath 461 85 moveto
+471 84 lineto
+462 90 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Indtypes -> Typeops
-newpath 194 45 moveto
-203 45 212 45 220 45 curveto
+newpath 193 67 moveto
+203 67 213 66 224 66 curveto
 stroke
-newpath 220 43 moveto
-230 45 lineto
-220 48 lineto
+newpath 221 64 moveto
+231 66 lineto
+221 69 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Instantiate
 gsave 10 dict begin
-716 45 39 18 ellipse_path
+716 72 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-716 46 moveto (Instantiate) 58 14.00 -0.50 alignedtext
+716 73 moveto (Instantiate) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Closure -> Instantiate
-newpath 640 45 moveto
-648 45 657 45 666 45 curveto
+newpath 640 72 moveto
+648 72 657 72 666 72 curveto
 stroke
-newpath 666 43 moveto
-676 45 lineto
-666 48 lineto
+newpath 666 70 moveto
+676 72 lineto
+666 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Environ
 gsave 10 dict begin
-825 72 33 18 ellipse_path
+825 99 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-825 73 moveto (Environ) 45 14.00 -0.50 alignedtext
+825 100 moveto (Environ) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Instantiate -> Environ
-newpath 751 54 moveto
-762 57 774 60 786 62 curveto
+newpath 751 81 moveto
+762 84 774 87 786 89 curveto
 stroke
-newpath 786 59 moveto
-795 65 lineto
-785 64 lineto
+newpath 786 86 moveto
+795 92 lineto
+785 91 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evd
 gsave 10 dict begin
-940 20 27 18 ellipse_path
+940 47 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-940 21 moveto (Evd) 22 14.00 -0.50 alignedtext
+940 48 moveto (Evd) 22 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Instantiate -> Evd
-newpath 755 41 moveto
-797 36 864 29 905 24 curveto
+newpath 755 68 moveto
+797 63 864 56 905 51 curveto
 stroke
-newpath 903 22 moveto
-913 23 lineto
-903 27 lineto
+newpath 903 49 moveto
+913 50 lineto
+903 54 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declarations
 gsave 10 dict begin
-940 74 45 18 ellipse_path
+940 101 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-940 75 moveto (Declarations) 70 14.00 -0.50 alignedtext
+940 102 moveto (Declarations) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Declarations
-newpath 858 73 moveto
-866 73 875 73 884 73 curveto
+newpath 858 100 moveto
+866 100 875 100 884 100 curveto
 stroke
-newpath 884 71 moveto
-894 73 lineto
-884 76 lineto
+newpath 884 98 moveto
+894 100 lineto
+884 103 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Evd -> Sign
-newpath 966 26 moveto
-980 29 998 34 1015 38 curveto
+newpath 966 53 moveto
+980 56 998 61 1015 65 curveto
 stroke
-newpath 1015 35 moveto
-1024 41 lineto
-1014 40 lineto
+newpath 1015 62 moveto
+1024 68 lineto
+1014 67 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declarations -> Sign
-newpath 979 64 moveto
-991 62 1003 59 1015 56 curveto
+newpath 979 91 moveto
+991 89 1003 86 1015 83 curveto
 stroke
-newpath 1014 54 moveto
-1024 53 lineto
-1015 59 lineto
+newpath 1014 81 moveto
+1024 80 lineto
+1015 86 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage