suppression des (* open Generic *)

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

68 files changed, 2 insertions, 72 deletions

diff --git a/Makefile b/Makefile
index 7c995fed3..854e73725 100644
--- a/Makefile
+++ b/Makefile
@@ -152,7 +152,7 @@ world: $(COQBINARIES) states theories contrib tools
 
 coqtop.opt: $(COQMKTOP) $(CMX) $(USERTACCMX)
 	$(COQMKTOP) -opt $(OPTFLAGS) -o coqtop.opt
-	$(STRIP) ./coqtop.opt
+#	$(STRIP) ./coqtop.opt
 
 coqtop.byte: $(COQMKTOP) $(CMO) $(USERTACCMO)
 	$(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 916810aa4..68eb6c2dc 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -9,7 +9,6 @@ open Sign
 open Univ
 open Proof_trees
 open Environ
-(* open Generic *)
 open Printer
 open Refiner
 open Tacmach
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 183afe253..f3f6ab8e4 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -4,7 +4,6 @@
 (*i*)
 open Pp
 open Names
-(* open Generic *)
 open Term
 open Evd
 open Environ
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 883e20f3f..ff80c338f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -3,7 +3,6 @@
 
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Sign
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index db7f78ba1..00e6d66f6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,6 @@ open Util
 open Names
 open Sign
 open Univ
-(* open Generic *)
 open Term
 open Declarations
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ba75b8b77..c4a5e4659 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -11,7 +11,7 @@ open Sign
 
 (*s Unsafe environments. We define here a datatype for environments. 
    Since typing is not yet defined, it is not possible to check the
-   informations added in environments, and that is what we speak here
+   informations added in environments, and that is why we speak here
    of ``unsafe'' environments. *)
 
 type context
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index acfea1109..f05d4922d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -3,7 +3,6 @@
 
 open Util
 open Names
-(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 94a8cc277..d319f633a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -4,7 +4,6 @@
 open Util
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index e6a25e6a3..e433423c0 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Evd
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5af00238f..dd2adf2f5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Univ
 open Evd
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 80dba1068..7908c26f2 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -3,7 +3,6 @@
 
 (*i*)
 open Names
-(* open Generic *)
 open Term
 open Univ
 open Evd
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index af46e221e..48d9ad184 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Reduction
 open Sign
diff --git a/kernel/sign.ml b/kernel/sign.ml
index eb2763645..96531ef49 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -3,7 +3,6 @@
 
 open Names
 open Util
-(* open Generic *)
 open Term
 
 (* Signatures *)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 29edde8f6..7ed3ae920 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -3,7 +3,6 @@
 
 (*i*)
 open Names
-(* open Generic *)
 open Term
 (*i*)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index c3ffb127b..97fe3c7dc 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -5,7 +5,6 @@
 open Util
 open Pp
 open Names
-(* open Generic *)
 (*i*)
 
 (*s The sorts of CCI. *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 463eb37a6..ce28a60a8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Declarations
 open Sign
diff --git a/library/declare.ml b/library/declare.ml
index e8aba9fe1..b46cf0e58 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/library/global.ml b/library/global.ml
index 52ea32986..118a189c6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 open Util
-(* open Generic *)
 open Term
 open Instantiate
 open Sign
diff --git a/library/impargs.ml b/library/impargs.ml
index 8dc830fae..b479dc5b9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 open Names
-(* open Generic *)
 open Term
 open Reduction
 open Declarations
diff --git a/library/indrec.ml b/library/indrec.ml
index a11ca751b..bbd4e62c2 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 377487710..cb707bd8d 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Sign
-(* open Generic *)
 open Term
 open Environ
 open Evd
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index ed8e9a5bf..d981109d5 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Environ
 
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 3db193625..0f552ca50 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 open Util
-(* open Generic *)
 open Names
 open Term
 open Reduction
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index a5d870a0b..75d6dc4ce 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 91111ada3..4591be556 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Univ
 open Names
-(* open Generic *)
 open Term
 open Inductive
 open Sign
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 413ea152a..84041fb32 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,7 +1,6 @@
 
 open Util
 open Names
-(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 0f201d004..0ea8e3113 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -4,7 +4,6 @@
 open Util
 open Pp
 open Names
-(* open Generic *)
 open Term
 open Inductive
 open Declarations
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 36b5ed4d5..249633cbd 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,6 @@ open Environ
 open Libobject
 open Declare
 open Term
-(* open Generic *)
 open Rawterm
 
 (* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6280fc392..ad518380d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,7 +1,6 @@
 (* $Id$ *)
 
 open Util
-(* open Generic *)
 open Names
 open Term
 open Reduction
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 70eba2949..3ed28a91e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Univ
 open Names
-(* open Generic *)
 open Term
 open Inductive
 open Sign
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fd52e0fa0..3316e2381 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -3,7 +3,6 @@
 
 open Util
 open Names
-(* open Generic *)
 open Term
 open Reduction
 open Instantiate
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ce08a0f39..72e46b52b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -5,7 +5,6 @@ open Util
 open Pp
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 67e793c54..510117330 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Sign
 open Evd
 open Term
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f16f77c63..9efd881fa 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -9,11 +9,6 @@ open Typeops
 open Libobject
 open Library
 open Classops
-(*
-open Pp_control
-(* open Generic *)
-open Initial
-*)
 
 let nbimpl = ref 0
 let nbpathc = ref 0
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 97c6c5306..8ad0203b3 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -4,7 +4,6 @@
 (*i*)
 open Names
 open Term
-(* open Generic *)
 open Classops
 open Libobject
 open Library
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 53bf5b08a..22eba722c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -5,7 +5,6 @@ open Util
 open Term
 open Inductive
 open Names
-(* open Generic *)
 open Reduction
 open Environ
 open Typeops
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 77f8cf9e1..653a08fdc 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Inductive
 open Environ
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 23028cc62..3f0ab9501 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -3,7 +3,6 @@
 
 open Util
 open Names
-(* open Generic *)
 open Term
 open Environ
 open Reduction
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 726042c35..962073127 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Instantiate
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index efeda72f3..7a9dbb177 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Stamps
 open Names
-(* open Generic *)
 open Term
 open Environ
 open Evd
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2bf95aed1..17eff5195 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Evd
-(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 62629a65b..be8446101 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Sign
-(* open Generic *)
 open Term
 open Declarations
 open Environ
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6a40e2c9d..1942b4264 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Stamps
-(* open Generic *)
 open Term
 open Sign
 open Evd
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 98f2b3554..09dc5a095 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -4,7 +4,6 @@
 open Astterm
 open Closure
 open Dyn
-(* open Generic *)
 open Libobject
 open Pattern
 open Pp
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4b2fcbc8e..6e0fafd8a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -4,7 +4,6 @@
 open Util
 open Stamps
 open Names
-(* open Generic *)
 open Sign
 open Term
 open Instantiate
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3e26eb9a7..a2a56fa9a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Inductive
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index ca1d0831a..237aee4be 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 (*i*)
-(* open Generic *)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 7e3ac13b2..42529c56a 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -107,7 +107,6 @@ Qed.
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Environ
 open Reduction
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e4b1ac15a..85ab52d1c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Reduction
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b4eaf03e8..b92e949d5 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Reduction
 open Inductive
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8c6ace2f6..6d4bc8d55 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Univ
-(* open Generic *)
 open Term
 open Inductive
 open Environ
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 944d82605..ba59183cb 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Reduction
 open Inductive
diff --git a/tactics/inv.ml b/tactics/inv.ml
index fa2602789..e2b2a0426 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Global
 open Sign
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 74f7bf2f2..962c18cc1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Evd
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index d5d657365..918313d0f 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -3,7 +3,6 @@
 
 open Util
 open Names
-(* open Generic *)
 open Term
 open Libobject
 open Library
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 4cbf696c4..038af44d2 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 (*i*)
-(* open Generic *)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 904ed3038..a63cfe975 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -42,7 +42,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Tacmach
 open Sign
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 0c513c2cf..5a5500fdc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e6b43a81e..34ad6e56c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,6 @@ open Util
 open Stamps
 open Names
 open Sign
-(* open Generic *)
 open Term
 open Inductive
 open Reduction
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 3a1df0234..481bd3ac4 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 open Util
-(* open Generic *)
 open Names
 open Term
 open Pattern
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 02415bc3c..8281a3179 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 (*i*)
-(* open Generic *)
 open Term
 open Pattern
 (*i*)
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index ab046025f..b67bf13f8 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Reduction
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 79f0df63a..577c29b05 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Options
-(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 765a63508..2e64ccab1 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Names
 open Sign
-(* open Generic *)
 open Term
 open Declarations
 open Inductive
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index aecec0c25..4f60a710c 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Environ
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1fe9d21ab..2a8805232 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -5,7 +5,6 @@ open Pp
 open Util
 open Options
 open Names
-(* open Generic *)
 open Term
 open Inductive
 open Indtypes
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 6276438e1..1807d9635 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Sign
 open Declarations
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 38d9e670d..559c3f33f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -4,7 +4,6 @@
 open Pp
 open Util
 open Names
-(* open Generic *)
 open Term
 open Declarations
 open Declare