Correction pour make doc

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

69 files changed, 71 insertions, 91 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
diff --git a/library/declare.ml b/library/declare.ml
index 9f98f3cb5a..5d62f067a7 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/library/global.ml b/library/global.ml
index 741d11e758..e58f1b03b9 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Util
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Instantiate
 open Sign
diff --git a/library/impargs.ml b/library/impargs.ml
index 3af4ecbecb..30e4c4e501 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Reduction
 open Declarations
diff --git a/library/indrec.ml b/library/indrec.ml
index ddba73abed..655db9af7e 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 9e5c86a528..6bd08a2ff8 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Reduction
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 72b7e1cf55..1a2cc53aef 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Sign
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Environ
 open Evd
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index f3aaa4e2a7..ed8e9a5bff 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Environ
 
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 17a4535a4d..f84a2d929c 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Util
-(*i open Generic i*)
+(* open Generic *)
 open Names
 open Term
 open Reduction
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 123f690a8b..d9e22af376 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0d04bd2b21..b8a39e37fa 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Univ
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Sign
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 54869505ee..1e48d3443c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,7 +1,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 5c56ce9b67..6c0da8c204 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -4,7 +4,7 @@
 open Util
 open Pp
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Declarations
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4e991a5fd5..f5af725b26 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,7 @@ open Environ
 open Libobject
 open Declare
 open Term
-(*i open Generic i*)
+(* open Generic *)
 open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d4a7ef4a68..7197110bf3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 open Util
-(*i open Generic i*)
+(* open Generic *)
 open Names
 open Term
 open Reduction
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a6d06f3f95..ce72f7e011 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Univ
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Sign
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f9a3fe69b0..4f551f31dd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Reduction
 open Instantiate
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2d35fb753c..e94ac55d39 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -5,7 +5,7 @@ open Util
 open Pp
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 295e081a34..41f1878d6b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Sign
 open Evd
 open Term
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 10c7cee073..f16f77c631 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -11,7 +11,7 @@ open Library
 open Classops
 (*
 open Pp_control
-(*i open Generic i*)
+(* open Generic *)
 open Initial
 *)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 0f90afeb5c..97c6c53069 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Term
-(*i open Generic i*)
+(* open Generic *)
 open Classops
 open Libobject
 open Library
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index bd1b88bea5..d6d3395e53 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -5,7 +5,7 @@ open Util
 open Term
 open Inductive
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Reduction
 open Environ
 open Typeops
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index dde27dbae8..87dca45db4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Environ
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cbe8b36013..99f2f09a8f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Environ
 open Reduction
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0cd364b93e..efc5190511 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Instantiate
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5cb4689aeb..3e2d96a957 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Stamps
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Environ
 open Evd
diff --git a/proofs/logic.ml b/proofs/logic.ml
index db9b7c1107..e06949be3f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Evd
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c660b35ef6..62629a65bb 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Sign
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Environ
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index badf6bc7a1..f54a8abb0f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Stamps
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Evd
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index b96f17af55..7375947f16 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -3,7 +3,7 @@
 
 open Astterm
 open Closure
-(*i open Generic i*)
+(* open Generic *)
 open Libobject
 open Pattern
 open Pp
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e8d4be64ef..ec3776c819 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -4,7 +4,7 @@
 open Util
 open Stamps
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Sign
 open Term
 open Instantiate
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e5dfff04c9..acf0b6cc6b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Inductive
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index aeb3f306ca..ca1d0831ac 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 4190cb17db..7e3ac13b29 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -107,7 +107,7 @@ Qed.
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Environ
 open Reduction
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6eab9ae082..09d8885d83 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Reduction
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 0fbfcae9a8..2cfcd8559c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Reduction
 open Inductive
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f325621820..bec81d44a8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Univ
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Environ
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd54744fe3..cc88fbcd7a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Reduction
 open Inductive
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 82863269bc..0a09c441bf 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Global
 open Sign
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 57baf0b154..c5bf517713 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.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/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index ae0f5a6c90..d5d657365f 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -3,7 +3,7 @@
 
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Libobject
 open Library
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index f68fc89e7f..4cbf696c4b 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index f5a95d59c1..08105aa9f0 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -42,7 +42,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Tacmach
 open Sign
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index b77ac413c8..d5ee7f9659 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4312071b48..a8693a70be 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@ open Util
 open Stamps
 open Names
 open Sign
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Reduction
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 416e81cd24..7c00a6b1d3 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -6,7 +6,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 9cdb34ab27..920e6ba310 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 open Util
-(*i open Generic i*)
+(* open Generic *)
 open Names
 open Term
 open Pattern
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 107026ef64..02415bc3c3 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 (*i*)
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 25c63e5366..4f071980e6 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Reduction
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2a15741bf6..e23d3b7f95 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Options
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 987daed1b3..9a55f5adfb 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Sign
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index bee6f074a9..92fb1bd93b 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a6e63497d0..cefa4d823d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Options
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Inductive
 open Indtypes
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index ab55fe549a..7e2b1f5bd6 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 30f7dbdee8..fbf2586525 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -4,7 +4,7 @@
 open Pp
 open Util
 open Names
-(*i open Generic i*)
+(* open Generic *)
 open Term
 open Declarations
 open Declare