diff options
68 files changed, 2 insertions, 72 deletions
@@ -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 916810aa45..68eb6c2dcf 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 183afe2538..f3f6ab8e41 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 883e20f3f4..ff80c338f9 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 db7f78ba11..00e6d66f6a 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 ba75b8b772..c4a5e4659e 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 acfea11092..f05d4922d3 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 94a8cc277e..d319f633ab 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 e6a25e6a3c..e433423c09 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 5af00238f3..dd2adf2f5f 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 80dba10682..7908c26f26 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 af46e221e2..48d9ad1848 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 eb27636452..96531ef496 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 29edde8f6b..7ed3ae9203 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 c3ffb127b4..97fe3c7dc0 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 463eb37a6a..ce28a60a86 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 e8aba9fe1f..b46cf0e581 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 52ea329860..118a189c6c 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 8dc830fae0..b479dc5b9c 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 a11ca751be..bbd4e62c2a 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 3774877101..cb707bd8d8 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 ed8e9a5bff..d981109d5f 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 3db193625f..0f552ca503 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 a5d870a0bc..75d6dc4ce1 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 91111ada39..4591be556d 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 413ea152a2..84041fb329 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 0f201d004f..0ea8e3113a 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 36b5ed4d53..249633cbdf 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 6280fc392b..ad518380dc 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 70eba2949e..3ed28a91e4 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 fd52e0fa0f..3316e23816 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 ce08a0f390..72e46b52b0 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 67e793c54f..5101173308 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 f16f77c631..9efd881fac 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 97c6c53069..8ad0203b35 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 53bf5b08a7..22eba722cc 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 77f8cf9e11..653a08fdc0 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 23028cc626..3f0ab9501a 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 726042c356..962073127d 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 efeda72f38..7a9dbb1772 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 2bf95aed11..17eff5195f 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 62629a65bb..be84461012 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 6a40e2c9d7..1942b42649 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 98f2b35545..09dc5a0955 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 4b2fcbc8ef..6e0fafd8a0 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 3e26eb9a7b..a2a56fa9a0 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 ca1d0831ac..237aee4be3 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 7e3ac13b29..42529c56a7 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 e4b1ac15ad..85ab52d1c5 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 b4eaf03e83..b92e949d5f 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 8c6ace2f61..6d4bc8d55a 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 944d826055..ba59183cb3 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 fa26027897..e2b2a0426f 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 74f7bf2f23..962c18cc17 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 d5d657365f..918313d0f7 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 4cbf696c4b..038af44d2d 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 904ed30382..a63cfe975e 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 0c513c2cf7..5a5500fdc6 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 e6b43a81e8..34ad6e56cd 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 3a1df02349..481bd3ac40 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 02415bc3c3..8281a31799 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 ab046025f8..b67bf13f89 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 79f0df63ad..577c29b058 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 765a63508a..2e64ccab17 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 aecec0c251..4f60a710c0 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 1fe9d21aba..2a88052326 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 6276438e10..1807d96356 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 38d9e670db..559c3f33f5 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 |