summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/autorewrite.mli4
-rw-r--r--tactics/btermdn.ml4
-rw-r--r--tactics/btermdn.mli4
-rw-r--r--tactics/class_tactics.ml44
-rw-r--r--tactics/contradiction.ml4
-rw-r--r--tactics/contradiction.mli4
-rw-r--r--tactics/decl_interp.ml6
-rw-r--r--tactics/decl_interp.mli4
-rw-r--r--tactics/decl_proof_instr.ml4
-rw-r--r--tactics/decl_proof_instr.mli4
-rw-r--r--tactics/dhyp.ml4
-rw-r--r--tactics/dhyp.mli4
-rw-r--r--tactics/eauto.ml44
-rw-r--r--tactics/eauto.mli2
-rw-r--r--tactics/elim.ml4
-rw-r--r--tactics/elim.mli4
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--tactics/elimschemes.mli5
-rw-r--r--tactics/eqdecide.ml44
-rw-r--r--tactics/eqschemes.ml4
-rw-r--r--tactics/eqschemes.mli4
-rw-r--r--tactics/equality.ml17
-rw-r--r--tactics/equality.mli4
-rw-r--r--tactics/evar_tactics.ml4
-rw-r--r--tactics/evar_tactics.mli4
-rw-r--r--tactics/extraargs.ml44
-rw-r--r--tactics/extraargs.mli4
-rw-r--r--tactics/extratactics.ml411
-rw-r--r--tactics/extratactics.mli4
-rw-r--r--tactics/hiddentac.ml4
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/hipattern.ml44
-rw-r--r--tactics/hipattern.mli4
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/inv.mli4
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/nbtermdn.ml4
-rw-r--r--tactics/nbtermdn.mli4
-rw-r--r--tactics/refine.ml4
-rw-r--r--tactics/refine.mli4
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--tactics/tacinterp.ml10
-rw-r--r--tactics/tacinterp.mli7
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tacticals.mli4
-rw-r--r--tactics/tactics.ml8
-rw-r--r--tactics/tactics.mli4
-rw-r--r--tactics/tauto.ml44
-rw-r--r--tactics/termdn.ml4
-rw-r--r--tactics/termdn.mli4
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