Imported Upstream version 8.3.pl3upstream/8.3.pl3

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