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 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;; |