diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /plugins | |
| 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 'plugins')
111 files changed, 0 insertions, 220 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 9b5fca4da..847b3f610 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 5f56c7e69..844bd43b5 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Term open Names diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 2a019ebff..e45e4e70a 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 2a0ca688c..6980ed8c6 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Ccalgo open Names open Term diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ccfa2a0a7..1ea1fdc64 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - (* This file is the interface between the c-c algorithm and Coq *) open Evd diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 7ed077bda..00ceac992 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Proof_type diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index d9db927a3..d65e339a3 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Cctac open Tactics open Tacticals diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 20a95dabf..b267fdc97 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - open Names open Util open Tacexpr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 2b583af40..1b91ef177 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Names open Topconstr diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli index bd0859382..bb008eaf8 100644 --- a/plugins/decl_mode/decl_interp.mli +++ b/plugins/decl_mode/decl_interp.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Tacinterp open Decl_expr open Mod_subst diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 90b0085ff..d71e356c7 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) - open Names open Term open Evd diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index fe485ce9b..0c24cd815 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - open Names open Term open Evd diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index cd695f239..97a56cabe 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Evd diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 0b22b7ac5..82df643d1 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Refiner open Names open Term diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index cdfc57b37..d87708510 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -9,8 +9,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) - (* arnaud: veiller à l'aspect tutorial des commentaires *) open Pp diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 40c712cdf..5bd15b93f 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Decl_expr diff --git a/plugins/dp/Dp.v b/plugins/dp/Dp.v index bc7d73f62..1b66c334e 100644 --- a/plugins/dp/Dp.v +++ b/plugins/dp/Dp.v @@ -6,8 +6,6 @@ Require Export Classical. (* Zenon *) (* Copyright 2004 INRIA *) -(* $Id$ *) - Lemma zenon_nottrue : (~True -> False). Proof. tauto. Qed. diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4 index 82f86cd81..e2cd4b3e3 100644 --- a/plugins/dp/g_dp.ml4 +++ b/plugins/dp/g_dp.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Dp TACTIC EXTEND Simplify diff --git a/plugins/dp/zenon.v b/plugins/dp/zenon.v index 502465c6b..89028c4f4 100644 --- a/plugins/dp/zenon.v +++ b/plugins/dp/zenon.v @@ -1,6 +1,4 @@ (* Copyright 2004 INRIA *) -(* $Id$ *) - Require Export Classical. Lemma zenon_nottrue : diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 73b51cfe7..18b3642e2 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.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/plugins/extraction/common.mli b/plugins/extraction/common.mli index a68e72d26..6d33bd8ea 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Libnames open Miniml diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 37721c9b9..33bac0e1c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Term open Declarations open Names diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index dcb4601e5..243fe4db3 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*s This module declares the extraction commands. *) open Names diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e7c2e23f7..e7b5f31fc 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Names diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 6bcd24763..7920a0302 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*s Extraction from Coq terms to Miniml. *) open Names diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 579f42df5..84202d539 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*s Production of Haskell syntax. *) open Pp diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli index 1b5dbc711..0a865bfcf 100644 --- a/plugins/extraction/haskell.mli +++ b/plugins/extraction/haskell.mli @@ -6,7 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - val haskell_descr : Miniml.language_descr diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 00df1a98d..effc7af46 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*s Target language for extraction: a core ML called MiniML. *) open Pp diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index df962773d..630a59e9d 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Pp open Util diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 0366c4ba7..8691d0181 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Names open Term diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9195b747e..7e8127fb3 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Declarations open Environ diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 8e04a368e..70d14fb27 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Declarations open Environ diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 5759cf0c2..3d980e65f 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*s Production of Ocaml syntax. *) open Pp diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli index 4a1c1778f..78cf59740 100644 --- a/plugins/extraction/ocaml.mli +++ b/plugins/extraction/ocaml.mli @@ -6,7 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - val ocaml_descr : Miniml.language_descr diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 9cc34634a..6a44812da 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*s Production of Scheme syntax. *) open Pp diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli index b0fa395c6..51c73ef14 100644 --- a/plugins/extraction/scheme.mli +++ b/plugins/extraction/scheme.mli @@ -6,6 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - val scheme_descr : Miniml.language_descr diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 866f499b5..36ba0cd7d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Term open Declarations diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 512ecca74..b8cdea3b6 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Libnames open Miniml diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v index efa53b4e9..bbc1e20b0 100644 --- a/plugins/field/LegacyField.v +++ b/plugins/field/LegacyField.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export LegacyField_Compl. Require Export LegacyField_Theory. Require Export LegacyField_Tactic. diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v index d4a39296a..1df77ef09 100644 --- a/plugins/field/LegacyField_Compl.v +++ b/plugins/field/LegacyField_Compl.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import List. Definition assoc_2nd := diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v index 5c1f228ac..50305d4a3 100644 --- a/plugins/field/LegacyField_Tactic.v +++ b/plugins/field/LegacyField_Tactic.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import List. Require Import LegacyRing. Require Export LegacyField_Compl. diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v index cc8b043fc..907b137a3 100644 --- a/plugins/field/LegacyField_Theory.v +++ b/plugins/field/LegacyField_Theory.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import List. Require Import Peano_dec. Require Import LegacyRing. diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 91c0ca21e..f08ed7db6 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Names open Pp open Proof_type diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 45365cb2c..3a2ca70b6 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Hipattern open Names open Term diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 2e89ddb06..77bc481a6 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Names open Libnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index f85616279..77f15aa07 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Formula open Sequent open Ground diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 7f4acb856..1d9b0c79a 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Formula open Sequent open Rules diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index 3c0e903fd..6722a7935 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - val ground_tac: Tacmach.tactic -> (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 810262a69..b473e5946 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Formula open Sequent open Unify diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 95dd22ea8..43a1b746c 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Term open Tacmach open Names diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 515efea70..fcc0f069b 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index fc32621ca..c5498fe0a 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Tacmach open Names diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 685d44a84..2f924198c 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Util open Formula diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index ce0eddccc..5e9f46aa2 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Util open Formula diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index e3a4c6a55..880e9a7d6 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Formula open Tacmach diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index d6cb3a082..60abdcd1a 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term exception UFAIL of constr*constr diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 07b2973a4..dc971aacf 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* "Fourier's method to solve linear inequations/equations systems.".*) Require Export LegacyRing. diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v index 0fd92d606..1974e51ab 100644 --- a/plugins/fourier/Fourier_util.v +++ b/plugins/fourier/Fourier_util.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Rbase. Comments "Lemmas used by the tactic Fourier". diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 73fb49295..21a5cb87f 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Méthode d'élimination de Fourier *) (* Référence: Auteur(s) : Fourier, Jean-Baptiste-Joseph diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 3f490babd..dc6463f42 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index b952851fa..705cc69e6 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open FourierR TACTIC EXTEND fourier diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c69e04b93..26f49f6d4 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -8,7 +8,6 @@ (* Merging of induction principles. *) -(*i $Id: i*) open Libnames open Tactics open Indfun_common diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8dc660b42..1780ff827 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Term open Termops open Namegen diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index f4d04e5d4..869ce84b9 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -14,8 +14,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Quote open Ring open Mutils diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v index 30b945718..6d0b6bae1 100644 --- a/plugins/omega/Omega.v +++ b/plugins/omega/Omega.v @@ -13,8 +13,6 @@ (* *) (**************************************************************************) -(* $Id$ *) - (* We do not require [ZArith] anymore, but only what's necessary for Omega *) Require Export ZArith_base. Require Export OmegaLemmas. diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index 56a854d6f..ff433bbd8 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id$ i*) - Require Import ZArith_base. Open Local Scope Z_scope. diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v index 21535f0d3..9ec850c0b 100644 --- a/plugins/omega/OmegaPlugin.v +++ b/plugins/omega/OmegaPlugin.v @@ -6,6 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Declare ML Module "omega_plugin". diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 60616845b..da2f27994 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,8 +13,6 @@ (* *) (**************************************************************************) -(* $Id$ *) - open Util open Pp open Reduction diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 3bfdce7fd..7751d767b 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -15,8 +15,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Coq_omega open Refiner diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index 11726675b..bb90f7f57 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Declare ML Module "quote_plugin". (*********************************************************************** diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index bdeb9844b..216b7840f 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Util open Tacexpr open Quote diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index ce65a45ec..6d096beec 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* The `Quote' tactic *) (* The basic idea is to automatize the inversion of interpetation functions diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 231b5fbb0..9572c1ce7 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Instantiation of the Ring tactic for the naturals of Arith $*) Require Import Bool. diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index ee9fb3761..eb62def87 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Instantiation of the Ring tactic for the binary natural numbers *) Require Import Bool. diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v index 4ae85baf3..cd51f9e02 100644 --- a/plugins/ring/LegacyRing.v +++ b/plugins/ring/LegacyRing.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Bool. Require Export LegacyRing_theory. Require Export Quote. diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index 30d29515f..a3071f7b4 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Bool. Set Implicit Arguments. diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index 68a0dd275..c48d61b0d 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Instantiation of the Ring tactic for the binary integers of ZArith *) Require Export LegacyArithRing. diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index 2a9df21b3..cccfe653b 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index 7aeee2185..54ddcb9ae 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import LegacyRing_theory. Require Import Quote. diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v index 93b9bc7cf..127228116 100644 --- a/plugins/ring/Setoid_ring.v +++ b/plugins/ring/Setoid_ring.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Setoid_ring_theory. Require Export Quote. Require Export Setoid_ring_normalize. diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index 9b4c46fe9..8d77854b6 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import Setoid_ring_theory. Require Import Quote. diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index 2c2314aff..0444fe74a 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Bool. Require Export Setoid. diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index d766e3445..99650a32f 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Quote open Ring open Tacticals diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index fdf3a9bd9..81f6b66ee 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* ML part of the Ring tactic *) open Pp diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 36da9463b..598b21d83 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export List. Require Export BinPos. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 0d1d09c73..47fc11825 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export List. Require Export Bintree. diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 4cbe84368..6309a7425 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$*) - (*i camlp4deps: "parsing/grammar.cma" i*) TACTIC EXTEND rtauto diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 562e2e3bd..029e7eafd 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Util open Goptions diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index e52f6bbdc..44a5f49c6 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - type form= Atom of int | Arrow of form * form diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 06313e8fe..3ae25da65 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - module Search = Explore.Make(Proof_search) open Util diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index a6d68a226..79872f2cd 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* raises Not_found if no proof is found *) type atom_env= diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index d6dece458..0f8c2f010 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index 406f94338..0dfeca511 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) open Environ open Tacmach open Term diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 index 700e61911..28ded30da 100644 --- a/plugins/subtac/g_subtac.ml4 +++ b/plugins/subtac/g_subtac.ml4 @@ -14,8 +14,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -(* $Id$ *) - open Flags open Util diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index e649ad97b..569aba263 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Global open Pp open Util diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 60e8cb0f7..4ec34a91a 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Cases open Util open Names diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 90989d2d3..4636bddc0 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Names diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 5c9deab8d..07b076e67 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Pretyping open Evd open Environ diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index ee78ff68a..6478d2065 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Names open Decl_kinds diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 9161d8887..6b07e3591 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -6,8 +6,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index 775397124..76229076c 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Global open Pp open Util diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index b49190d44..4d7bcb1eb 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 19473dfa6..79e1a6eb2 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.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/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 5d20c2a3c..932b20f38 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* This file defines the printer for natural numbers in [nat] *) (*i*) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 4375d5e0f..826b5c384 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index f85309e67..38e0a159f 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.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/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index bc02357ae..cb2b16858 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.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/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index f6afd080f..7d5ee96d1 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pcoq open Pp open Util diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli index 3775287a5..195b37bbc 100644 --- a/plugins/xml/xml.mli +++ b/plugins/xml/xml.mli @@ -12,8 +12,6 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i $Id$ i*) - (* Tokens for XML cdata, empty elements and not-empty elements *) (* Usage: *) (* Str cdata *) diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli index 66ff9f0bb..1a6aea97b 100644 --- a/plugins/xml/xmlcommand.mli +++ b/plugins/xml/xmlcommand.mli @@ -12,8 +12,6 @@ (* http://helm.cs.unibo.it *) (************************************************************************) -(*i $Id$ i*) - (* print_global qid fn *) (* where qid is a long name denoting a definition/theorem or *) (* an inductive definition *) diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index 41c107ad2..ec1613144 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -14,8 +14,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Util;; open Vernacinterp;; |