diff options
| author |  Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
| commit | 300293c119981054c95182a90c829058530a6b6f (patch) | |
| tree | d7303613741c5796b58ced7db24ec7203327dbb2 /tactics | |
| parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) | |
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'tactics')
53 files changed, 136 insertions, 108 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index ca2f4916..6a9ced3e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 13390 2010-09-02 08:03:01Z herbelin $ *) +(* $Id: auto.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/auto.mli b/tactics/auto.mli index 9a0719fc..eef6a0ee 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: auto.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 09f80377..2a41a8e5 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: autorewrite.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: autorewrite.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Equality open Hipattern diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index b7300cba..ec285500 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: autorewrite.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: autorewrite.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 73aac029..119d8398 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: btermdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: btermdn.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Term open Names diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 14f9fb23..22d3c3a2 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: btermdn.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: btermdn.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 66f15fbe..465d1d80 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 13902 2011-03-10 15:50:24Z msozeau $ *) +(* $Id: class_tactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9ea4892e..f459a3dd 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: contradiction.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: contradiction.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Term diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 7306f875..bd2138d5 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: contradiction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: contradiction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 7866d640..c4cff4d7 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decl_interp.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: decl_interp.ml 14677 2011-11-17 22:19:38Z herbelin $ i*) open Util open Names @@ -28,7 +28,7 @@ let intern_justification_items globs = Option.map (List.map (intern_constr globs)) let intern_justification_method globs = - Option.map (intern_tactic globs) + Option.map (intern_pure_tactic globs) let intern_statement intern_it globs st = {st_label=st.st_label; diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli index 859db444..e2c1e531 100644 --- a/tactics/decl_interp.mli +++ b/tactics/decl_interp.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_interp.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: decl_interp.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Tacinterp open Decl_expr diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index f9a51afe..5a89e859 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: decl_proof_instr.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index 6f8126ed..5af60a1b 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: decl_proof_instr.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Refiner open Names diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 5b7e7e94..041e58df 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dhyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: dhyp.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Chet's comments about this tactic : diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index a4be2e42..4cde3b49 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dhyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: dhyp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 2b25ad73..e0cdbcfa 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: eauto.ml4 13344 2010-07-28 15:04:36Z msozeau $ *) +(* $Id: eauto.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/eauto.mli b/tactics/eauto.mli index eb90b1b6..b40261b6 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/elim.ml b/tactics/elim.ml index 0372a88d..f3517ea6 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: elim.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: elim.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/elim.mli b/tactics/elim.mli index fa18ab0b..c6aecad7 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: elim.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: elim.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index c82e8f64..c60938ed 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: elimschemes.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: elimschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index ba0389e5..ab01a5fa 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: elimschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: elimschemes.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Ind_tables @@ -16,6 +16,7 @@ val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind val rect_dep_scheme_kind_from_type : individual scheme_kind +val ind_scheme_kind_from_type : individual scheme_kind val ind_dep_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 90e4b44c..a16e99bb 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,7 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: eqdecide.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: eqdecide.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 22c3b47f..88931415 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: eqschemes.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: eqschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* File created by Hugo Herbelin, Nov 2009 *) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 447fb359..08b3b05c 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eqschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: eqschemes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* This file builds schemes relative to equality inductive types *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 411ccc0e..a25f88e3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *) +(* $Id: equality.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -681,10 +681,21 @@ let gen_absurdity id gl = absurd_term=False *) +let ind_scheme_of_eq lbeq = + let ind = destInd lbeq.eq in + let (mib,mip) = Global.lookup_inductive ind in + let kind = inductive_sort_family mip in + (* use ind rather than case by compatibility *) + let kind = + if kind = InProp then Elimschemes.ind_scheme_kind_from_prop + else Elimschemes.ind_scheme_kind_from_type in + mkConst (find_scheme kind ind) + + let discrimination_pf e (t,t1,t2) discriminator lbeq = let i = build_coq_I () in let absurd_term = build_coq_False () in - let eq_elim = lbeq.ind in + let eq_elim = ind_scheme_of_eq lbeq in (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) exception NotDiscriminable diff --git a/tactics/equality.mli b/tactics/equality.mli index f14b3867..0c2d8942 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: equality.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: equality.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 825ec492..9f7c0a54 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_tactics.ml 13428 2010-09-17 18:03:40Z herbelin $ *) +(* $Id: evar_tactics.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Term open Util diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index 78412150..f54f6a4c 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evar_tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: evar_tactics.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Tacmach open Names diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index c9b2a969..310423d2 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extraargs.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: extraargs.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Pcoq diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index e53fc604..a3f27fde 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraargs.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: extraargs.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Tacexpr open Term diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index dfc8b6bf..c4a2ef44 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 13658 2010-11-29 11:09:05Z glondu $ *) +(* $Id: extratactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Pcoq @@ -662,3 +662,10 @@ TACTIC EXTEND has_evar | [ "has_evar" constr(x) ] -> [ if has_evar x then tclIDTAC else tclFAIL 0 (str "No evars") ] END + +TACTIC EXTEND is_hyp +| [ "is_var" constr(x) ] -> + [ match kind_of_term x with + | Var _ -> tclIDTAC + | _ -> tclFAIL 0 (str "Not a variable or hypothesis") ] +END diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index cfbc8f3d..ecad939c 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extratactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: extratactics.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Proof_type diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 220c00d3..018bf815 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hiddentac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: hiddentac.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Term open Proof_type diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 1724bf9c..31484cc0 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hiddentac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: hiddentac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index dfa596d3..08bcf65a 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) -(* $Id: hipattern.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: hipattern.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index cf4cdd0d..15d7bfc6 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hipattern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: hipattern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/tactics/inv.ml b/tactics/inv.ml index 430f7d5f..37142f30 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: inv.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/inv.mli b/tactics/inv.mli index eb899699..43e2a8de 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inv.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: inv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 76432dd8..2544a4be 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: leminv.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index bdea29df..19df4ff1 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nbtermdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: nbtermdn.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index 36c54bd3..e655b6e3 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nbtermdn.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: nbtermdn.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/tactics/refine.ml b/tactics/refine.ml index 06a78011..c1b1fe9d 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refine.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: refine.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* JCF -- 6 janvier 1998 EXPERIMENTAL *) diff --git a/tactics/refine.mli b/tactics/refine.mli index 55b4033b..15491616 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: refine.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: refine.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Tacmach diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 360be9ef..fd3eeeb2 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ba9a5173..6a11384b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 13489 2010-10-03 22:27:12Z herbelin $ *) +(* $Id: tacinterp.ml 14677 2011-11-17 22:19:38Z herbelin $ *) open Constrintern open Closure @@ -995,6 +995,12 @@ and intern_genarg ist x = | None -> lookup_genarg_glob s ist x +let intern_pure_tactic ist a = + match intern_tactic ist a with + | TacArg (TacCall _ | TacExternal _ | Reference _ | TacDynamic _ | Tacexp _) as a -> a + | TacArg _ | TacFun _ -> error "Tactic expected." + | a -> a + (************* End globalization ************) (***************************************************************************) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 82f4d99a..8f585781 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: tacinterp.mli 14677 2011-11-17 22:19:38Z herbelin $ i*) (*i*) open Pp @@ -102,6 +102,9 @@ val intern_genarg : val intern_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr +val intern_pure_tactic : + glob_sign -> raw_tactic_expr -> glob_tactic_expr + val intern_constr : glob_sign -> constr_expr -> rawconstr_and_expr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 171a35c0..f0d4dc51 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacticals.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: tacticals.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index af74e382..6466ab78 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacticals.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: tacticals.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 771047fd..186b5c48 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 13981 2011-04-08 16:59:26Z herbelin $ *) +(* $Id: tactics.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -1708,8 +1708,8 @@ let letin_tac_gen with_eq name c ty occs gl = tclTHENLIST [ convert_concl_no_check newcl DEFAULTcast; intro_gen dloc (IntroMustBe id) lastlhyp true false; - eq_tac; - tclMAP convert_hyp_no_check depdecls ] gl + tclMAP convert_hyp_no_check depdecls; + eq_tac ] gl let letin_tac with_eq name c ty occs = letin_tac_gen with_eq name c ty (occs,true) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index bfc32654..5ceade1f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: tactics.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index a7e7613d..a17aba76 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: tauto.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*) open Term open Hipattern diff --git a/tactics/termdn.ml b/tactics/termdn.ml index f9f086d9..17329b6f 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: termdn.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/tactics/termdn.mli b/tactics/termdn.mli index e778de8d..ccfa91a9 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termdn.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: termdn.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term |