diff options
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 |