documentation

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

1 files changed, 180 insertions, 203 deletions

diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 1a694e765c..8a9253ae9e 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: Bill Gates
+%%For: (jc) Jean-Christophe,,,,
 %%Title: G
 %%Pages: (atend)
-%%BoundingBox: 36 36 577 131
+%%BoundingBox: 36 36 577 94
 %%EndComments
 %%BeginProlog
 save
@@ -139,408 +139,385 @@ def
 % /arrowwidth 5 def
 %%EndSetup
 %%Page: 1 1
-%%PageBoundingBox: 36 36 577 131
+%%PageBoundingBox: 36 36 577 94
 gsave
-35 35 542 96 boxprim clip newpath
+35 35 542 59 boxprim clip newpath
 36 36 translate
 0 0 1 beginpage
-0.4787 set_scale
+0.4000 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
-999 98 27 18 ellipse_path
+1221 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-999 99 moveto (Univ) 28 14.00 -0.50 alignedtext
+1221 73 moveto (Univ) 28 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Names
 gsave 10 dict begin
-1098 71 29 18 ellipse_path
+1320 45 29 18 ellipse_path
 stroke
 gsave 10 dict begin
-1098 72 moveto (Names) 38 14.00 -0.50 alignedtext
+1320 46 moveto (Names) 38 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Univ -> Names
-newpath 1024 91 moveto
-1036 88 1049 84 1062 81 curveto
+newpath 1246 65 moveto
+1258 62 1271 58 1284 55 curveto
 stroke
-newpath 1061 79 moveto
-1071 78 lineto
-1062 84 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Typing
-gsave 10 dict begin
-31 98 30 18 ellipse_path
-stroke
-gsave 10 dict begin
-31 99 moveto (Typing) 40 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Indtypes
-gsave 10 dict begin
-133 125 34 18 ellipse_path
-stroke
-gsave 10 dict begin
-133 126 moveto (Indtypes) 48 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Typing -> Indtypes
-newpath 59 105 moveto
-69 108 81 111 92 114 curveto
-stroke
-newpath 93 112 moveto
-102 117 lineto
-92 117 lineto
+newpath 1283 53 moveto
+1293 52 lineto
+1284 58 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Typeops
 gsave 10 dict begin
-133 71 34 18 ellipse_path
+265 70 34 18 ellipse_path
 stroke
 gsave 10 dict begin
-133 72 moveto (Typeops) 48 14.00 -0.50 alignedtext
+265 71 moveto (Typeops) 48 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Typing -> Typeops
-newpath 59 91 moveto
-69 88 81 85 92 82 curveto
-stroke
-newpath 92 79 moveto
-102 79 lineto
-93 84 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
 %	Reduction
 gsave 10 dict begin
-243 125 39 18 ellipse_path
+375 97 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-243 126 moveto (Reduction) 57 14.00 -0.50 alignedtext
+375 98 moveto (Reduction) 57 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
-%	Indtypes -> Reduction
-newpath 168 125 moveto
-176 125 185 125 194 125 curveto
-stroke
-newpath 194 123 moveto
-204 125 lineto
-194 128 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
 %	Typeops -> Reduction
-newpath 158 83 moveto
-173 91 192 100 208 108 curveto
+newpath 296 78 moveto
+307 80 319 83 330 86 curveto
 stroke
-newpath 208 105 moveto
-216 112 lineto
-206 110 lineto
+newpath 331 84 moveto
+340 89 lineto
+330 89 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Type_errors
 gsave 10 dict begin
-363 71 44 18 ellipse_path
+495 45 44 18 ellipse_path
 stroke
 gsave 10 dict begin
-363 72 moveto (Type_errors) 68 14.00 -0.50 alignedtext
+495 46 moveto (Type_errors) 68 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Typeops -> Type_errors
-newpath 168 71 moveto
-205 71 265 71 309 71 curveto
+newpath 299 66 moveto
+337 62 399 55 443 51 curveto
 stroke
-newpath 308 69 moveto
-318 71 lineto
-308 74 lineto
+newpath 442 49 moveto
+452 50 lineto
+442 54 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Closure
 gsave 10 dict begin
-363 125 32 18 ellipse_path
+495 99 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-363 126 moveto (Closure) 43 14.00 -0.50 alignedtext
+495 100 moveto (Closure) 43 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Reduction -> Closure
-newpath 282 125 moveto
-295 125 309 125 321 125 curveto
+newpath 414 98 moveto
+427 98 441 98 453 98 curveto
 stroke
-newpath 321 123 moveto
-331 125 lineto
-321 128 lineto
+newpath 453 96 moveto
+463 98 lineto
+453 101 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Environ
 gsave 10 dict begin
-593 99 33 18 ellipse_path
+815 72 33 18 ellipse_path
 stroke
 gsave 10 dict begin
-593 100 moveto (Environ) 45 14.00 -0.50 alignedtext
+815 73 moveto (Environ) 45 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Type_errors -> Environ
-newpath 406 76 moveto
-447 81 511 89 552 94 curveto
+newpath 539 49 moveto
+601 54 713 63 774 68 curveto
 stroke
-newpath 550 91 moveto
-560 95 lineto
-550 96 lineto
+newpath 772 65 moveto
+782 69 lineto
+772 70 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Inductive
 gsave 10 dict begin
-705 180 36 18 ellipse_path
+927 126 36 18 ellipse_path
 stroke
 gsave 10 dict begin
-705 181 moveto (Inductive) 52 14.00 -0.50 alignedtext
+927 127 moveto (Inductive) 52 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Inductive
-newpath 611 114 moveto
-626 127 648 145 662 156 curveto
-665 158 669 161 674 163 curveto
-stroke
-newpath 673 159 moveto
-680 167 lineto
-670 164 lineto
-closepath
-gsave 0 setgray stroke grestore fill
-
-%	Evd
-gsave 10 dict begin
-705 126 27 18 ellipse_path
-stroke
-gsave 10 dict begin
-705 127 moveto (Evd) 22 14.00 -0.50 alignedtext
-end grestore
-end grestore
-
-%	Environ -> Evd
-newpath 623 106 moveto
-638 109 655 114 670 118 curveto
+newpath 840 84 moveto
+855 92 875 101 892 109 curveto
 stroke
-newpath 670 115 moveto
-679 120 lineto
-669 120 lineto
+newpath 893 107 moveto
+901 113 lineto
+891 111 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Abstraction
 gsave 10 dict begin
-705 18 43 18 ellipse_path
+927 18 43 18 ellipse_path
 stroke
 gsave 10 dict begin
-705 19 moveto (Abstraction) 65 14.00 -0.50 alignedtext
+927 19 moveto (Abstraction) 65 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Abstraction
-newpath 611 84 moveto
-626 71 648 53 662 42 curveto
-665 40 668 38 672 36 curveto
+newpath 840 60 moveto
+854 53 874 44 890 36 curveto
 stroke
-newpath 668 35 moveto
-678 32 lineto
-671 40 lineto
+newpath 889 34 moveto
+899 32 lineto
+891 38 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Constant
 gsave 10 dict begin
-705 72 35 18 ellipse_path
+927 72 35 18 ellipse_path
 stroke
 gsave 10 dict begin
-705 73 moveto (Constant) 49 14.00 -0.50 alignedtext
+927 73 moveto (Constant) 49 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Environ -> Constant
-newpath 623 92 moveto
-635 89 650 86 663 82 curveto
+newpath 848 72 moveto
+859 72 871 72 882 72 curveto
 stroke
-newpath 663 80 moveto
-673 80 lineto
-664 84 lineto
+newpath 882 70 moveto
+892 72 lineto
+882 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Term
 gsave 10 dict begin
-903 71 27 18 ellipse_path
+1125 45 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-903 72 moveto (Term) 30 14.00 -0.50 alignedtext
+1125 46 moveto (Term) 30 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Univ
-newpath 928 78 moveto
-939 81 953 85 965 88 curveto
+newpath 1150 52 moveto
+1161 55 1175 59 1187 62 curveto
 stroke
-newpath 965 85 moveto
-974 91 lineto
-964 90 lineto
+newpath 1187 59 moveto
+1196 65 lineto
+1186 64 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Generic
 gsave 10 dict begin
-999 44 32 18 ellipse_path
+1221 18 32 18 ellipse_path
 stroke
 gsave 10 dict begin
-999 45 moveto (Generic) 44 14.00 -0.50 alignedtext
+1221 19 moveto (Generic) 44 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Term -> Generic
-newpath 928 64 moveto
-938 61 949 58 960 55 curveto
+newpath 1150 38 moveto
+1160 35 1171 32 1182 29 curveto
 stroke
-newpath 960 52 moveto
-970 52 lineto
-961 57 lineto
+newpath 1182 26 moveto
+1192 26 lineto
+1183 31 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Generic -> Names
-newpath 1028 52 moveto
-1038 55 1051 58 1062 61 curveto
+newpath 1250 26 moveto
+1260 29 1273 32 1284 35 curveto
 stroke
-newpath 1062 58 moveto
-1071 64 lineto
-1061 63 lineto
+newpath 1284 32 moveto
+1293 38 lineto
+1283 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sosub
 gsave 10 dict begin
-812 31 27 18 ellipse_path
+1034 18 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-812 32 moveto (Sosub) 34 14.00 -0.50 alignedtext
+1034 19 moveto (Sosub) 34 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sosub -> Term
-newpath 835 41 moveto
-846 46 860 52 872 57 curveto
+newpath 1059 26 moveto
+1069 29 1080 32 1091 35 curveto
 stroke
-newpath 872 54 moveto
-880 61 lineto
-870 59 lineto
+newpath 1091 32 moveto
+1100 38 lineto
+1090 37 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Sign
 gsave 10 dict begin
-812 112 27 18 ellipse_path
+1034 72 27 18 ellipse_path
 stroke
 gsave 10 dict begin
-812 113 moveto (Sign) 25 14.00 -0.50 alignedtext
+1034 73 moveto (Sign) 25 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Sign -> Term
-newpath 834 102 moveto
-845 97 859 91 872 85 curveto
+newpath 1059 65 moveto
+1069 62 1080 58 1091 55 curveto
 stroke
-newpath 871 83 moveto
-881 81 lineto
-873 87 lineto
+newpath 1090 53 moveto
+1100 53 lineto
+1091 58 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Safe_typing
+gsave 10 dict begin
+44 70 44 18 ellipse_path
+stroke
+gsave 10 dict begin
+44 71 moveto (Safe_typing) 67 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Indtypes
+gsave 10 dict begin
+159 70 34 18 ellipse_path
+stroke
+gsave 10 dict begin
+159 71 moveto (Indtypes) 48 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Safe_typing -> Indtypes
+newpath 88 70 moveto
+97 70 106 70 114 70 curveto
+stroke
+newpath 114 68 moveto
+124 70 lineto
+114 73 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+%	Indtypes -> Typeops
+newpath 194 70 moveto
+203 70 212 70 220 70 curveto
+stroke
+newpath 220 68 moveto
+230 70 lineto
+220 73 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Instantiate
 gsave 10 dict begin
-484 123 39 18 ellipse_path
+616 98 39 18 ellipse_path
 stroke
 gsave 10 dict begin
-484 124 moveto (Instantiate) 58 14.00 -0.50 alignedtext
+616 99 moveto (Instantiate) 58 14.00 -0.50 alignedtext
 end grestore
 end grestore
 
 %	Closure -> Instantiate
-newpath 395 124 moveto
-407 124 421 124 434 124 curveto
+newpath 527 99 moveto
+539 99 553 98 566 98 curveto
 stroke
-newpath 434 122 moveto
-444 124 lineto
-434 127 lineto
+newpath 566 96 moveto
+576 98 lineto
+566 101 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Instantiate -> Environ
-newpath 520 115 moveto
-530 113 542 110 553 108 curveto
+%	Evd
+gsave 10 dict begin
+719 96 27 18 ellipse_path
+stroke
+gsave 10 dict begin
+719 97 moveto (Evd) 22 14.00 -0.50 alignedtext
+end grestore
+end grestore
+
+%	Instantiate -> Evd
+newpath 656 97 moveto
+665 97 674 97 682 97 curveto
 stroke
-newpath 552 106 moveto
-562 106 lineto
-553 111 lineto
+newpath 682 95 moveto
+692 97 lineto
+682 100 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Inductive -> Sign
-newpath 730 167 moveto
-736 163 743 159 748 156 curveto
-754 152 772 140 787 129 curveto
+%	Evd -> Environ
+newpath 744 90 moveto
+754 88 765 85 775 82 curveto
 stroke
-newpath 783 128 moveto
-793 125 lineto
-786 133 lineto
+newpath 775 80 moveto
+785 80 lineto
+776 84 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
-%	Evd -> Sign
-newpath 732 123 moveto
-745 121 761 119 776 117 curveto
+%	Inductive -> Sign
+newpath 953 113 moveto
+968 105 988 96 1004 87 curveto
 stroke
-newpath 775 115 moveto
-785 115 lineto
-776 120 lineto
+newpath 1002 85 moveto
+1012 83 lineto
+1004 90 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Abstraction -> Sosub
-newpath 746 23 moveto
-756 24 766 25 776 27 curveto
+newpath 970 18 moveto
+979 18 988 18 996 18 curveto
 stroke
-newpath 775 24 moveto
-785 28 lineto
-775 29 lineto
+newpath 996 16 moveto
+1006 18 lineto
+996 21 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 
 %	Constant -> Sign
-newpath 733 83 moveto
-747 88 765 94 779 100 curveto
+newpath 962 72 moveto
+974 72 986 72 997 72 curveto
 stroke
-newpath 779 97 moveto
-788 103 lineto
-778 102 lineto
+newpath 997 70 moveto
+1007 72 lineto
+997 75 lineto
 closepath
 gsave 0 setgray stroke grestore fill
 endpage