diff options
Diffstat (limited to 'plugins')
111 files changed, 0 insertions, 220 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 9b5fca4da1..847b3f6102 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 5f56c7e69f..844bd43b50 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 2a019ebfff..e45e4e70af 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 2a0ca688c6..6980ed8c6e 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 ccfa2a0a70..1ea1fdc640 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 7ed077bda1..00ceac992b 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 d9db927a37..d65e339a3a 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 20a95dabff..b267fdc979 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 2b583af407..1b91ef1776 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 bd0859382b..bb008eaf8f 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 90b0085ffa..d71e356c75 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 fe485ce9b6..0c24cd815b 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 cd695f239d..97a56cabe6 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 0b22b7ac53..82df643d16 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 cdfc57b374..d87708510f 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 40c712cdff..5bd15b93fa 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 bc7d73f62d..1b66c334eb 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 82f86cd81a..e2cd4b3e3e 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 502465c6be..89028c4f4c 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 73b51cfe7d..18b3642e28 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 a68e72d261..6d33bd8ea0 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 37721c9b96..33bac0e1c3 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 dcb4601e58..243fe4db34 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 e7c2e23f7d..e7b5f31fce 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 6bcd24763f..7920a0302b 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 579f42df5b..84202d5398 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 1b5dbc7111..0a865bfcf2 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 00df1a98d3..effc7af468 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 df962773d0..630a59e9d8 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 0366c4ba78..8691d01815 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 9195b747e9..7e8127fb3e 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 8e04a368ed..70d14fb274 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 5759cf0c2a..3d980e65f0 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 4a1c1778f2..78cf597409 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 9cc34634a9..6a44812da3 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 b0fa395c63..51c73ef14f 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 866f499b59..36ba0cd7d8 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 512ecca743..b8cdea3b6a 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 efa53b4e9d..bbc1e20b01 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 d4a39296a0..1df77ef095 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 5c1f228ac6..50305d4a38 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 cc8b043fce..907b137a3e 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 91c0ca21ec..f08ed7db61 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 45365cb2cd..3a2ca70b67 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 2e89ddb061..77bc481a68 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 f85616279d..77f15aa07a 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 7f4acb8564..1d9b0c79a8 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 3c0e903fdc..6722a79353 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 810262a699..b473e5946e 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 95dd22ea89..43a1b746c2 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 515efea701..fcc0f069b1 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 fc32621ca7..c5498fe0a1 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 685d44a84d..2f924198c2 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 ce0eddccc2..5e9f46aa28 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 e3a4c6a559..880e9a7d6d 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 d6cb3a082d..60abdcd1a0 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 07b2973a4a..dc971aacff 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 0fd92d6064..1974e51aba 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 73fb49295a..21a5cb87fe 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 3f490babd7..dc6463f426 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 b952851fae..705cc69e6e 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 c69e04b938..26f49f6d49 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 8dc660b421..1780ff8275 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 f4d04e5d48..869ce84b92 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 30b9457183..6d0b6bae1a 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 56a854d6f8..ff433bbd83 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 21535f0d3b..9ec850c0ba 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 60616845be..da2f279945 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 3bfdce7fdc..7751d767b8 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 11726675b3..bb90f7f573 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 bdeb9844be..216b7840fe 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 ce65a45ec8..6d096beecf 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 231b5fbb0f..9572c1ce7b 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 ee9fb37615..eb62def87d 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 4ae85baf37..cd51f9e022 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 30d29515f0..a3071f7b43 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 68a0dd2758..c48d61b0df 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 2a9df21b33..cccfe653be 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 7aeee21857..54ddcb9aea 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 93b9bc7cf5..1272281162 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 9b4c46fe92..8d77854b6c 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 2c2314affe..0444fe74ab 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 d766e34454..99650a32ff 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 fdf3a9bd9d..81f6b66ee1 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 36da9463ba..598b21d834 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 0d1d09c736..47fc118259 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 4cbe843685..6309a74256 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 562e2e3bdb..029e7eafd1 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 e52f6bbdc5..44a5f49c68 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 06313e8fe7..3ae25da653 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 a6d68a2265..79872f2cdc 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 d6dece458b..0f8c2f010b 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 406f94338b..0dfeca5112 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 700e619118..28ded30dac 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 e649ad97be..569aba2637 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 60e8cb0f7c..4ec34a91ad 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 90989d2d31..4636bddc08 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 5c9deab8df..07b076e673 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 ee78ff68a4..6478d20650 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 9161d88870..6b07e3591c 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 7753971244..76229076ca 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 b49190d446..4d7bcb1ebd 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 19473dfa69..79e1a6eb2c 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 5d20c2a3c8..932b20f38a 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 4375d5e0f4..826b5c3844 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 f85309e671..38e0a159f2 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 bc02357aea..cb2b168587 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 f6afd080f4..7d5ee96d13 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 3775287a5d..195b37bbca 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 66ff9f0bbd..1a6aea97b5 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 41c107ad2c..ec1613144d 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;; |