Correction pour make doc

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

15 files changed, 17 insertions, 37 deletions

diff --git a/kernel/abstraction.ml b/kernel/abstraction.ml
index a6e5937a47..04ed649920 100644
--- a/kernel/abstraction.ml
+++ b/kernel/abstraction.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 
 type abstraction_body = { 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 940cd2664f..d9353abfa2 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Pp
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Evd
 open Environ
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index a5cb164d06..9c6ffb1725 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -3,7 +3,7 @@
 
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 604d0aea36..257cba2b14 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@ open Util
 open Names
 open Sign
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Abstraction
@@ -310,21 +310,7 @@ let make_all_name_different env =
        push_rel (Name id,c,t) newenv)
     env
 
-(* Abstractions. *)
-(*
-let evaluable_abst env = function
-  | DOPN (Abst _,_) -> true
-  | _ -> invalid_arg "evaluable_abst"
-
-let translucent_abst env = function
-  | DOPN (Abst _,_) -> false
-  | _ -> invalid_arg "translucent_abst"
-
-let abst_value env = function
-  | DOPN(Abst sp, args) ->
-      contract_abstraction (lookup_abst sp env) args
-  | _ -> invalid_arg "abst_value"
-*)
+(* Constants *)
 let defined_constant env = function
   | DOPN (Const sp, _) -> is_defined (lookup_constant sp env)
   | _ -> invalid_arg "defined_constant"
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a37e469bd9..534a95c944 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index db3329a1a8..569b681e9a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -4,7 +4,7 @@
 open Util
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 9b1d9289a5..ed625a22f0 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Evd
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 352e41e382..0d88ccc73c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Univ
 open Evd
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 01d42fc079..37a05bbe5e 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -3,7 +3,7 @@
 
 (*i*)
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Univ
 open Evd
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 68cd846b75..e0c951c224 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Reduction
 open Sign
diff --git a/kernel/sign.ml b/kernel/sign.ml
index eac5c8cc9a..27aa150e62 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -3,7 +3,7 @@
 
 open Names
 open Util
-(*i open Generic i*)
+(* open Generic *)
 open Term
 
 (* Signatures *)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 889c79b4e0..bb2e083de7 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -3,7 +3,7 @@
 
 (*i*)
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 (*i*)
 
diff --git a/kernel/sosub.ml b/kernel/sosub.ml
index 7212216ee5..4ea19e8212 100644
--- a/kernel/sosub.ml
+++ b/kernel/sosub.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 (*
 (* Given a term with variables in it, and second-order substitution,
diff --git a/kernel/term.mli b/kernel/term.mli
index e4e0e1df5c..fe3996c5c6 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -5,7 +5,7 @@
 open Util
 open Pp
 open Names
-(*i open Generic i*)
+(* open Generic *)
 (*i*)
 
 (*s The sorts of CCI. *)
@@ -76,7 +76,7 @@ and typed_type
 
 type flat_arity = (name * constr) list * sorts
 
-(*s Functions about typed_type *)
+(*s Functions about [typed_type] *)
 
 val make_typed : constr -> sorts -> typed_type
 val make_typed_lazy : constr -> (constr -> sorts) -> typed_type
@@ -358,12 +358,6 @@ val args_of_const : constr -> constr array
 val destEvar : constr -> int * constr array
 val num_of_evar : constr -> int
 
-(*
-(* Destructs an abstract term *)
-val destAbst : constr -> section_path * constr array
-val path_of_abst : constr -> section_path
-val args_of_abst : constr -> constr array
-*)
 (* Destructs a (co)inductive type *)
 val destMutInd : constr -> inductive
 val op_of_mind : constr -> inductive_path
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 37dfccf9ee..078b6b96b1 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Sign