diff --git a/Makefile b/Makefile index 0c9bccc83c3f..03b6e576f2a2 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# unit diff --git a/checker/cic.mli b/checker/cic.mli index 1f4322dff1f6..42629ced2726 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Names.ModPath.t -> Cic.module_body -> unit diff --git a/checker/modops.ml b/checker/modops.ml index f0abc39eac44..c7ad0977ac42 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Values.value -> 'a -> unit diff --git a/checker/values.ml b/checker/values.ml index 283adca0329b..160653d9bcd4 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int type 'a eq = 'a -> 'a -> bool diff --git a/clib/cList.mli b/clib/cList.mli index b3ee28548c31..db37050aa912 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int type 'a eq = 'a -> 'a -> bool diff --git a/clib/cMap.ml b/clib/cMap.ml index b4c4aedd0e48..373e3f8fdac3 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string list Util.String.Map.t -> unit diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index eb575b95ff5d..55d8d9698013 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GText.tag -> unit) -> string -> unit diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index fcc242e074e9..1fdd7317b5c8 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit diff --git a/ide/document.ml b/ide/document.ml index 62457fe56bcf..0d3b36a7fd48 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GMisc.image diff --git a/ide/interface.mli b/ide/interface.mli index a5d98946f382..debbc8301ed2 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* () diff --git a/ide/minilib.mli b/ide/minilib.mli index 4f5fbe7db70b..6cc36f5f2a0f 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string diff --git a/ide/preferences.ml b/ide/preferences.ml index 7c251f79c6a9..11aaf6e8ccd0 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 6a9e238797c9..6e36ae1c8ae3 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Coq.coqtop -> CoqOps.coqops -> diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index f87730461f77..6a9317bc2fd8 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GText.view -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 65df2b849452..74f687ef76f3 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit diff --git a/interp/genintern.ml b/interp/genintern.ml index 2f2edab30ceb..161201c448d3 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* diff --git a/lib/future.mli b/lib/future.mli index 853f81cea0bf..d9e8c87b212f 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index c262e50e5bb7..ae0605cfb7c5 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit Proofview.tactic diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 609ca62a0406..5db587b9ccbb 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* : non commutative polynomials on a commutative ring A *) diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 25afeaa7f5ea..795850781980 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Entries.mutual_inductive_entry -> diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 86bc471323fb..1664e68f2bda 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* diff --git a/printing/prettyp.mli b/printing/prettyp.mli index c1d8f1d37a58..213f0aeeb67c 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 04062fbbd62b..d6b386f1036c 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Cdglobals.coq_module -> unit diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 186f6cf6cf52..1be440a75074 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* on 9 & 10 Mar 2004: diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d043c4a58410..d252270021d9 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*