diff options
52 files changed, 81 insertions, 47 deletions
diff --git a/contrib/dp/Dp.v b/contrib/dp/Dp.v index db028a5ea2..47d67725f2 100644 --- a/contrib/dp/Dp.v +++ b/contrib/dp/Dp.v @@ -6,7 +6,7 @@ Require Export Classical. (* Zenon *) (* Copyright 2004 INRIA *) -(* $Id: zenon.v,v 1.6 2006-02-16 09:22:46 doligez Exp $ *) +(* $Id$ *) Lemma zenon_nottrue : (~True -> False). diff --git a/contrib/dp/zenon.v b/contrib/dp/zenon.v index 2ef9436755..502465c6be 100644 --- a/contrib/dp/zenon.v +++ b/contrib/dp/zenon.v @@ -1,5 +1,5 @@ (* Copyright 2004 INRIA *) -(* $Id: zenon.v,v 1.6 2006-02-16 09:22:46 doligez Exp $ *) +(* $Id$ *) Require Export Classical. diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index 39eaa0b98b..c5f8509759 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -280,7 +280,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacExact c | TacExactNoCheck c | TacVmCastNoCheck c -> depends_of_'constr c acc - | TacApply (_, cb) -> depends_of_'constr_with_bindings cb acc + | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc | TacElim (_, cwb, cwbo) -> depends_of_'constr_with_bindings cwb (Option.fold_right depends_of_'constr_with_bindings cwbo acc) diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v index dc8635bdf9..ed1da9c56e 100644 --- a/contrib/ring/LegacyRing.v +++ b/contrib/ring/LegacyRing.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) Require Export Bool. Require Export LegacyRing_theory. diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 5b8bb9c0f8..1bc5897c45 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 9399 2006-11-22 16:11:53Z herbelin $ *) +(* $Id$ *) open Cases open Util diff --git a/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli index 02fe016d63..90989d2d31 100644 --- a/contrib/subtac/subtac_cases.mli +++ b/contrib/subtac/subtac_cases.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cases.mli 8741 2006-04-26 22:30:32Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Util diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index d652436802..0bff421383 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) open Pretyping open Evd diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index c621f1516f..9a6730454a 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 0a0e144bd8..2610f10368 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 9ecdcd6c07..018c471d40 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h index ba8a601491..04e38656f3 100644 --- a/kernel/byterun/int64_emul.h +++ b/kernel/byterun/int64_emul.h @@ -11,7 +11,7 @@ /* */ /***********************************************************************/ -/* $Id: int64_emul.h,v 1.5 2005/09/22 14:21:50 xleroy Exp $ */ +/* $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 2341e99891..f5bef4a6f4 100644 --- a/kernel/byterun/int64_native.h +++ b/kernel/byterun/int64_native.h @@ -11,7 +11,7 @@ /* */ /***********************************************************************/ -/* $Id: int64_native.h,v 1.5 2005/09/22 14:21:50 xleroy Exp $ */ +/* $Id$ */ /* Wrapper macros around native 64-bit integer arithmetic, so that it has the same interface as the software emulation diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index b82556c78b..44f5dcb32d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retroknowledge.ml ??? 2006-??-?? ??:??:??Z spiwack $ *) +(* $Id$ *) open Term open Names diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 999bf0ede2..2baf382854 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: retroknowledge.mli ??? 2006-??-?? ??:??:??Z spiwack $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/kernel/vm.ml b/kernel/vm.ml index c1d3ca56fd..665e00a305 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + open Names open Term open Conv_oracle diff --git a/lib/flags.ml b/lib/flags.ml index 12b2ed0370..6a801480a2 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: options.ml 10106 2007-08-30 16:56:10Z herbelin $ *) +(*i $Id:$ i*) open Util diff --git a/lib/flags.mli b/lib/flags.mli index 248b59b0df..73962735da 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: options.mli 9679 2007-02-24 15:22:07Z herbelin $ i*) +(*i $Id$ i*) (* Global options of the system. *) diff --git a/lib/option.ml b/lib/option.ml index 95a18396bb..543c108ab9 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id:$ i*) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index b1a8ae3485..4528fde9cb 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $ $ i*) +(*i $Id:$ i*) (* digit-based syntax for int31, bigN bigZ and bigQ *) diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index 4564790388..3218781d12 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id:$ i*) + open Pp open Util open Names diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml index 6d879fb204..6b1faa76ce 100644 --- a/parsing/g_string_syntax.ml +++ b/parsing/g_string_syntax.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +(*i $Id:$ i*) + open Pp open Util open Names diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index b076220b45..64062765a0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -365,8 +365,12 @@ GEXTEND Gram | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c - | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl) - | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl) + | IDENT "apply"; cl = constr_with_bindings -> TacApply (true,false,cl) + | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,true,cl) + | IDENT "simple"; IDENT "apply"; cl = constr_with_bindings -> + TacApply (false,false,cl) + | IDENT "simple"; IDENT "eapply"; cl = constr_with_bindings -> + TacApply (false, true,cl) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (false,cl,el) | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 497b8a3c60..44ca8eb2cb 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *) +(* $Id$ *) open Rawterm open Term diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 922c7af163..55b5315851 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -295,8 +295,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> - | Tacexpr.TacApply (false,cb) -> - <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >> + | Tacexpr.TacApply (b,false,cb) -> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9d837df0ee..4c944f4608 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id:$ i*) (*i*) open Names diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 193f3ae3c2..2646c09dde 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index ae806cbf57..dc3f81f56f 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id:$ i*) (*i*) open Names diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index f97aed96a8..d93a354eca 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c746e41999..384c4b221d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id:$ i*) + open Names open Declarations open Term diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml index b83f9dc658..cdb7b0675e 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) +(*i $Id:$ i*) open Names open Term diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 96df8f6418..16bca302e7 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id:$ i*) + open Names open Constrextern open Pp diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 6a8d0d36d3..5c24224774 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: eauto.ml4 10346 2007-12-05 21:11:19Z aspiwack $ *) +(* $Id$ *) open Pp open Util diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index b33fbde8aa..4eb59a2fb0 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id:$ i*) open Util open Names diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 014f6ffcd5..5e86abe7bf 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -51,7 +51,7 @@ Abort. (* Check insertion of coercions in bindings *) -Coercion eq_true : bool >-> Sortclass. +(*Coercion eq_true : bool >-> Sortclass.*) Goal exists A:Prop, A = A. exists true. trivial. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index d215bccb9e..fd8576a8cd 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index a4c97fc82d..0ec6c11f99 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Require Export Coq.Program.Basics. Require Import Coq.Program.Tactics. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 4750df6399..64eee17d8e 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Require Import Coq.Classes.RelationClasses. Require Import Coq.Classes.Morphisms. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index cb27fbc380..43320dcebc 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) -(* $Id: Init.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *) diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index c7e199b62b..3a029371b4 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 0c663b7093..6ef2f756d3 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -14,7 +14,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index 7cf2980c41..17bd4a6d72 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Require Import Coq.Program.Program. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index d370ffa441..f7f460123e 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 842d32fdbc..639b15f506 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 8d2be43cc8..38bdc0bc92 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 1129c5b65e..8f1f26dbcd 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - Universitﾃツopyright Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) (** The polymorphic identity function. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 46a1b5cf25..0f88fbdd93 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index c2a6f3df6c..440217bfec 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 10410 2007-12-31 13:11:55Z msozeau $ i*) +(*i $Id$ i*) (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index f54a6c286a..2e51ef9734 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qring.v 9427 2006-12-11 18:46:35Z bgregoir $ i*) +(*i $Id$ i*) Require Export Field. Require Export QArith_base. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 05d7857c4e..9feac54111 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id:$ i*) + open Tacmach open Util open Flags diff --git a/toplevel/classes.ml b/toplevel/classes.ml index eda8760a94..535dda6238 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/toplevel/classes.mli b/toplevel/classes.mli index da00044d90..c259971414 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index fe3bddf376..ae4e8cf52c 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id:$ i*) + open Names open Mod_subst |