diff options
| author | letouzey | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /kernel | |
| parent | 0f61b02f84b41e1f019cd78824de28f18ff854aa (diff) | |
Remove the svn-specific $Id$ annotations
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
51 files changed, 0 insertions, 102 deletions
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h index 04e38656f3..86bee72edb 100644 --- a/kernel/byterun/int64_emul.h +++ b/kernel/byterun/int64_emul.h @@ -11,8 +11,6 @@ /* */ /***********************************************************************/ -/* $Id$ */ - /* Software emulation of 64-bit integer arithmetic, for C compilers that do not support it. */ diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h index f5bef4a6f4..8a6a266457 100644 --- a/kernel/byterun/int64_native.h +++ b/kernel/byterun/int64_native.h @@ -11,8 +11,6 @@ /* */ /***********************************************************************/ -/* $Id$ */ - /* Wrapper macros around native 64-bit integer arithmetic, so that it has the same interface as the software emulation provided in int64_emul.h */ diff --git a/kernel/closure.ml b/kernel/closure.ml index 93788ed422..e77ea4cb33 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Term diff --git a/kernel/closure.mli b/kernel/closure.mli index ce339ab331..d482e91b2f 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Names open Term diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 0851c7a5f9..5e9db9c7d2 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Names (* Priority for the expansion of constant in the conversion test. diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 35e09072f0..0e8201694b 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names (** Order on section paths for unfolding. diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 7605df9eb2..7b380944bf 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 5f30bce62b..42991d5071 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Declarations diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 515009798c..0762a92d19 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Names diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c6cf8a7511..15c5350b07 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Univ open Term diff --git a/kernel/entries.ml b/kernel/entries.ml index 938d1c60aa..fb84218cc4 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Names open Univ diff --git a/kernel/entries.mli b/kernel/entries.mli index 2cfdf93140..78316dd9b7 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Univ open Term diff --git a/kernel/environ.ml b/kernel/environ.ml index 8f6a619a0a..69220908ef 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Sign diff --git a/kernel/environ.mli b/kernel/environ.mli index fce149e10e..0ecfa21b6a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Declarations diff --git a/kernel/esubst.ml b/kernel/esubst.ml index c8b5fb269e..fd07d92971 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util (*********************) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index bbb3d838e8..fd7753093f 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Sect } *) (** Explicit substitutions of type ['a]. - ESID(n) = %n END bounded identity diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 10cedbf59e..90ddd984d0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Univ diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index c29e5475d4..388eb21e42 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Univ open Term diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 76de25344e..9215ac0c66 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Univ diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 7f2b088447..259e1decd4 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Univ open Term diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 5cb53d166b..8abfe09437 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 53925955e8..e22a3eb7d0 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 [Mod_subst] } *) open Names diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c9d9ac9242..e67b987a6f 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Names open Univ diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 188e4809cf..10619820e3 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Declarations open Environ open Entries diff --git a/kernel/modops.ml b/kernel/modops.ml index 2d9c92afc7..084fdd4f41 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Pp diff --git a/kernel/modops.mli b/kernel/modops.mli index 0c61e773bc..3ab2961d21 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Univ diff --git a/kernel/names.ml b/kernel/names.ml index 06ca87b4da..dfa73e95a1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util diff --git a/kernel/names.mli b/kernel/names.mli index f712c8d19f..ffbc027140 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Identifiers } *) type identifier diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index b58951e983..3835c81c51 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Sign diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 619c1afcbc..9078558a9d 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: pre_env.mli 12406 2009-10-21 15:12:52Z soubiran {% $ %} *) - open Util open Names open Sign diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 92386c4d36..4a4661f996 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 06d4478b25..a6ebda4918 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Environ open Closure diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index a3e493db9f..c0f714f96c 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Names diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 19f30cd8fe..0634a99aa1 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d9c7c9de04..cffe7e7722 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Univ diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 2aad2eb8c9..ce62eeafcc 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Declarations diff --git a/kernel/sign.ml b/kernel/sign.ml index d30d70860e..f987a1f6c9 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Names open Util open Term diff --git a/kernel/sign.mli b/kernel/sign.mli index 5cadb125f9..07f3df19e6 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e07af3ba33..9bc719e7e7 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Names diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index d68d908a00..061a6eb0b9 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Univ open Declarations open Environ diff --git a/kernel/term.ml b/kernel/term.ml index d0e9d16950..a1effb317e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* This module instantiates the structure of generic deBruijn terms to Coq *) open Util diff --git a/kernel/term.mli b/kernel/term.mli index 830e7e5ed4..3940d74c5a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c465adfac2..dac8ee47af 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Univ diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index d1fc71eb5c..49463e75a0 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Univ diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 2d26d27e1b..77b69bb88f 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Names open Term open Sign diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index ed2ec13022..dabff83606 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Environ diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 27db208c65..231ea2b16d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Univ diff --git a/kernel/typeops.mli b/kernel/typeops.mli index a89aae4d28..e2df7e983b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Univ open Term diff --git a/kernel/univ.ml b/kernel/univ.ml index 0a22733d05..f42b6fb939 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 1d85386c5b..3a2ec557fb 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Universes. *) type universe diff --git a/kernel/vm.ml b/kernel/vm.ml index 338936250c..1f57457d74 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Names open Term open Conv_oracle |