diff options
Diffstat (limited to 'tactics')
50 files changed, 0 insertions, 100 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index d2bb1a06fc..32a199e607 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/auto.mli b/tactics/auto.mli index 37fe3d4418..f7c3fd7775 100644 --- a/tactics/auto.mli +++ b/tactics/auto.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/tactics/autorewrite.ml b/tactics/autorewrite.ml index a0dea0292e..2b05fcb65f 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Equality open Hipattern open Names diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index a9556891a6..bda1fc65f3 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Tacexpr open Tacmach diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index bcb9a411c0..13027fd348 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Names open Termdn diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index ebb046a05f..a4ace7637b 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Pattern open Names diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e0e7aae2fe..18d2c60814 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -9,8 +9,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 46ed2134d0..29604a95f2 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Term open Proof_type diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index b5fdf5a1bc..b74a23271c 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Proof_type diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 96d83b9724..f45685eafc 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Chet's comments about this tactic : Programmable destruction of hypotheses and conclusions. diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 465a2a377e..c35b4d759d 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Tacmach open Tacexpr diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 49af8b40ea..ebef403a17 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/elim.ml b/tactics/elim.ml index cac200f58d..7baa5cd8c4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/elim.mli b/tactics/elim.mli index 7fbb16ba1a..2351947e06 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Proof_type diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e3f29fe596..28c6960101 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent Siles (decidable equality and boolean equality) and Matthieu Sozeau diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index ef1c4ec3e2..d58878838e 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: elimschemes.mli 12584 2009-12-13 21:04:34Z herbelin {% $ %} *) - open Ind_tables (** Induction/recursion schemes *) diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index d5e4ca17d7..a93be7bc69 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -14,8 +14,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Util open Names open Namegen diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 51dbd7ecdd..195d4b7c44 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* File created by Hugo Herbelin, Nov 2009 *) (* This file builds schemes related to equality inductive types, diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index bdf3bbe76c..8c649aecf4 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** This file builds schemes relative to equality inductive types *) open Names diff --git a/tactics/equality.ml b/tactics/equality.ml index 8a4fb392ea..1a5a92fc3f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/equality.mli b/tactics/equality.mli index b5c147393d..d5694ba899 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Names diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 906c32c57a..c8e6c9769c 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Util open Evar_refiner diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 0cf4dbb809..ffce595477 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Tacmach open Names open Tacexpr diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index adf8275ee8..dd37822a1f 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Pp open Pcoq open Genarg diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 3421ded92a..ffa1bd747c 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Tacexpr open Term open Names diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 8a68c9f20d..a1c1da177e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Pp open Pcoq open Genarg diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 259fe8814f..f2f13fe11b 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Proof_type val h_discrHyp : Names.identifier -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 4fed5d27cf..da2b49557f 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Proof_type open Tacmach diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index dae0281bdb..120d42abf6 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -7,8 +7,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Util open Term diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index b6112c34fb..b203839697 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 40ad0da9ba..3fa8596f90 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.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/tactics/inv.ml b/tactics/inv.ml index 46ca8161c8..3130c1ca9b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/inv.mli b/tactics/inv.mli index a7780206ba..b038e4f0e3 100644 --- a/tactics/inv.mli +++ b/tactics/inv.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/tactics/leminv.ml b/tactics/leminv.ml index 395a7c206e..5c22bfd894 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 7d6e1c4c90..67b396dda2 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index 3f866d5da2..5d80d847eb 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Pattern open Libnames diff --git a/tactics/refine.ml b/tactics/refine.ml index cb6cb961f4..484954bcc7 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* JCF -- 6 janvier 1998 EXPERIMENTAL *) (* diff --git a/tactics/refine.mli b/tactics/refine.mli index c9a4598e59..ef369a8572 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Tacmach val refine : Evd.open_constr -> tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 1af2d33988..fd34d70f97 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -9,8 +9,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: rewrite.ml4 11981 2009-03-16 08:18:53Z herbelin $ *) - open Pp open Util open Names diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 6e3957ac05..86bd7cbee8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Constrintern open Closure open RedFlags diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 771d28fbac..7c731e2b9c 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index 8e5124c417..ff3abd1d2d 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 12623 2010-01-04 17:50:38Z letouzey $ *) - open Libobject open Proof_type open Pp diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli index 208a76aefb..d74bb0ebb6 100644 --- a/tactics/tactic_option.mli +++ b/tactics/tactic_option.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 12623 2010-01-04 17:50:38Z letouzey $ *) - open Proof_type open Tacexpr open Vernacexpr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 045f70c61b..1ff67bffe5 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index c357451a21..e67e11227a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e6201aad9d..21a9ee258e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2d7c074029..8a413e1370 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.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/tactics/tauto.ml4 b/tactics/tauto.ml4 index 60baa017cf..2bb225c667 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id$ i*) - open Term open Hipattern open Names diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 7b6d3ea767..fe5dc572dc 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Nameops diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 973cc0e5b6..ed3a928abb 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Pattern open Libnames |