nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes

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

1 files changed, 69 insertions, 59 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 7b66406111..692a28e87c 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: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 70
+%%BoundingBox: 36 36 576 73
 %%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,41 +139,41 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 70
+%%PageBoundingBox: 36 36 576 73
 gsave
-35 35 542 35 boxprim clip newpath
+35 35 541 38 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.3745 set_scale
+0.3994 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
-1319 45 27 18 ellipse_path
+1229 47 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1319 46 moveto (Univ) 28 14.00 -0.50 alignedtext
+1229 48 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1412 45 29 18 ellipse_path
+1322 47 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1412 46 moveto (Names) 38 14.00 -0.50 alignedtext
+1322 48 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1346 45 moveto
-1354 45 1363 45 1372 45 curveto
+newpath 1256 47 moveto
+1264 47 1273 47 1282 47 curveto
 stroke
-newpath 1372 43 moveto
-1382 45 lineto
-1372 48 lineto
+newpath 1282 45 moveto
+1292 47 lineto
+1282 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -274,39 +274,39 @@ gsave 0 setgray stroke grestore fill
 
 %	Term
 gsave 10 dict begin
-1229 45 27 18 ellipse_path
+1139 47 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1229 46 moveto (Term) 30 14.00 -0.50 alignedtext
+1139 48 moveto (Term) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Univ
-newpath 1256 45 moveto
-1264 45 1273 45 1282 45 curveto
+newpath 1166 47 moveto
+1174 47 1183 47 1192 47 curveto
 stroke
-newpath 1282 43 moveto
-1292 45 lineto
-1282 48 lineto
+newpath 1192 45 moveto
+1202 47 lineto
+1192 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sign
 gsave 10 dict begin
-1139 45 27 18 ellipse_path
+1049 47 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-1139 46 moveto (Sign) 25 14.00 -0.50 alignedtext
+1049 48 moveto (Sign) 25 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sign -> Term
-newpath 1166 45 moveto
-1174 45 1183 45 1192 45 curveto
+newpath 1076 47 moveto
+1084 47 1093 47 1102 47 curveto
 stroke
-newpath 1192 43 moveto
-1202 45 lineto
-1192 48 lineto
+newpath 1102 45 moveto
+1112 47 lineto
+1102 50 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
@@ -367,70 +367,80 @@ newpath 666 43 moveto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evd
+%	Environ
 gsave 10 dict begin
-819 45 27 18 ellipse_path
+825 72 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-819 46 moveto (Evd) 22 14.00 -0.50 alignedtext
+825 73 moveto (Environ) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Instantiate -> Evd
-newpath 756 45 moveto
-765 45 774 45 782 45 curveto
+%	Instantiate -> Environ
+newpath 751 54 moveto
+762 57 774 60 786 62 curveto
 stroke
-newpath 782 43 moveto
-792 45 lineto
-782 48 lineto
+newpath 786 59 moveto
+795 65 lineto
+785 64 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Environ
+%	Evd
 gsave 10 dict begin
-915 45 33 18 ellipse_path
+940 20 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-915 46 moveto (Environ) 45 14.00 -0.50 alignedtext
+940 21 moveto (Evd) 22 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Evd -> Environ
-newpath 846 45 moveto
-854 45 863 45 872 45 curveto
+%	Instantiate -> Evd
+newpath 755 41 moveto
+797 36 864 29 905 24 curveto
 stroke
-newpath 872 43 moveto
-882 45 lineto
-872 48 lineto
+newpath 903 22 moveto
+913 23 lineto
+903 27 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declarations
 gsave 10 dict begin
-1030 45 45 18 ellipse_path
+940 74 45 18 ellipse_path
 stroke
 gsave 10 dict begin
-1030 46 moveto (Declarations) 70 14.00 -0.50 alignedtext
+940 75 moveto (Declarations) 70 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Declarations
-newpath 948 45 moveto
-956 45 965 45 974 45 curveto
+newpath 858 73 moveto
+866 73 875 73 884 73 curveto
+stroke
+newpath 884 71 moveto
+894 73 lineto
+884 76 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Evd -> Sign
+newpath 966 26 moveto
+980 29 998 34 1015 38 curveto
 stroke
-newpath 974 43 moveto
-984 45 lineto
-974 48 lineto
+newpath 1015 35 moveto
+1024 41 lineto
+1014 40 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Declarations -> Sign
-newpath 1076 45 moveto
-1085 45 1094 45 1102 45 curveto
+newpath 979 64 moveto
+991 62 1003 59 1015 56 curveto
 stroke
-newpath 1102 43 moveto
-1112 45 lineto
-1102 48 lineto
+newpath 1014 54 moveto
+1024 53 lineto
+1015 59 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage