From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 proofs/clenv.ml         |  2 +-
 proofs/clenv.mli        |  2 +-
 proofs/clenvtac.ml      |  6 +++---
 proofs/clenvtac.mli     |  2 +-
 proofs/evar_refiner.ml  |  2 +-
 proofs/evar_refiner.mli |  2 +-
 proofs/goal.ml          |  2 +-
 proofs/goal.mli         |  2 +-
 proofs/logic.ml         |  2 +-
 proofs/logic.mli        |  2 +-
 proofs/pfedit.ml        |  5 +++--
 proofs/pfedit.mli       |  2 +-
 proofs/proof.ml         | 18 ++++++++++++++++--
 proofs/proof.mli        | 11 ++++++++++-
 proofs/proof_global.ml  |  2 +-
 proofs/proof_global.mli |  2 +-
 proofs/proof_type.ml    |  2 +-
 proofs/proof_type.mli   |  2 +-
 proofs/proofview.ml     |  7 ++++++-
 proofs/proofview.mli    | 20 +++++++++++++++++++-
 proofs/redexpr.ml       |  2 +-
 proofs/redexpr.mli      |  2 +-
 proofs/refiner.ml       |  2 +-
 proofs/refiner.mli      |  2 +-
 proofs/tacexpr.ml       | 14 +++++++++-----
 proofs/tacmach.ml       |  2 +-
 proofs/tacmach.mli      |  2 +-
 proofs/tactic_debug.ml  |  2 +-
 proofs/tactic_debug.mli |  2 +-
 29 files changed, 88 insertions(+), 37 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index b98101e0..6af908ee 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index abd67236..7722544a 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index eb935d05..ca8fd6ae 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -71,8 +71,8 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
     if with_classes then
-      Typeclasses.resolve_typeclasses ~fail:(not with_evars)
-	clenv.env clenv.evd
+      Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
+        ~fail:(not with_evars) clenv.env clenv.evd
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 49a961f5..b4cd77c2 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6fa95dc8..4462062c 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 8e7c0713..6cdd46e0 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index eeaba76e..dc1ac5dd 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 50709555..9cd439ab 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5babd03a..d240c1e1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 420e6374..696115a8 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6ac0b553..5e314069 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -64,7 +64,8 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
   let goals = [ (Global.env_of_context hyps , c) ] in
   let init_tac = Option.map Proofview.V82.tactic init_tac in
   Proof_global.start_proof id str goals ?compute_guard hook;
-  Option.iter Proof_global.run_tactic init_tac
+  try Option.iter Proof_global.run_tactic init_tac
+  with e -> Proof_global.discard_current (); raise e
 
 let restart_proof () = undo_todepth 1
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5d45ea7c..89e12c01 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 996a895f..a4e556c5 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -149,12 +149,26 @@ type proof = { (* current proof_state *)
 
 (*** General proof functions ***)
 
+let proof { state = p } =
+  let (goals,sigma) = Proofview.proofview p.proofview in
+  (* spiwack: beware, the bottom of the stack is used by [Proof]
+     internally, and should not be exposed. *)
+  let rec map_minus_one f = function
+    | [] -> assert false
+    | [_] -> []
+    | a::l -> f a :: (map_minus_one f l)
+  in
+  let stack =
+    map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
+  in
+  (goals,stack,sigma)
+
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
 
 (* spiwack: a proof is considered completed even if its still focused, if the focus
-                   doesn't hide any goal.
+   doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
 let is_done p =
   Proofview.finished p.state.proofview && 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 715b3341..2e7c7a5a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -34,6 +34,15 @@ open Term
 (* Type of a proof. *)
 type proof
 
+(* Returns a stylised view of a proof for use by, for instance,
+   ide-s. *)
+(* spiwack: the type of [proof] will change as we push more refined
+   functions to ide-s. This would be better than spawning a new nearly
+   identical function everytime. Hence the generic name. *)
+(* In this version: returns the focused goals, a representation of the
+   focus stack (the number of goals at each level) and the underlying
+   evar_map *)
+val proof : proof -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Evd.evar_map
 
 (*** General proof functions ***)
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ae0f7d12..6cc5f9dc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e266d57c..cf97955e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e256794a..468effeb 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 2b0a10ba..262f183b 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4246cc9c..74e40e3b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,6 +29,9 @@ type proofview = {
      comb : Goal.goal list
      }
 
+let proofview p =
+  p.comb , p.solution
+
 (* Initialises a proofview, the argument is a list of environement, 
    conclusion types, and optional names, creating that many initial goals. *)
 let init = 
@@ -96,6 +99,8 @@ let list_goto =
    order) *)
 type focus_context = Goal.goal list * Goal.goal list
 
+let focus_context f = f
+
 (* This (internal) function extracts a sublist between two indices, and
    returns this sublist together with its context:
    if it returns [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index fe24b54b..fb215c52 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,6 +24,16 @@ open Term
 
 type proofview 
 
+
+(* Returns a stylised view of a proofview for use by, for instance,
+   ide-s. *)
+(* spiwack: the type of [proofview] will change as we push more
+   refined functions to ide-s. This would be better than spawning a
+   new nearly identical function everytime. Hence the generic name. *)
+(* In this version: returns the list of focused goals together with
+   the [evar_map] context. *)
+val proofview : proofview -> Goal.goal list * Evd.evar_map
+
 (* Initialises a proofview, the argument is a list of environement, 
    conclusion types, creating that many initial goals. *)
 val init : (Environ.env * Term.types) list -> proofview
@@ -46,6 +56,14 @@ exception IndexOutOfRange
 (* Type of the object which allow to unfocus a view.*)
 type focus_context
 
+(* Returns a stylised view of a focus_context for use by, for
+   instance, ide-s. *)
+(* spiwack: the type of [focus_context] will change as we push more
+   refined functions to ide-s. This would be better than spawning a
+   new nearly identical function everytime. Hence the generic name. *)
+(* In this version: returns the number of goals that are held *)
+val focus_context : focus_context -> Goal.goal list * Goal.goal list
+
 (* [focus i j] focuses a proofview on the goals from index [i] to index [j] 
    (inclusive). (i.e. goals number [i] to [j] become the only goals of the
    returned proofview).
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0430a239..d5750cfa 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index ae82153d..fec9840d 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8901a5a2..37c63644 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9d3d37c2..4e30c9c0 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index de2e662f..1be0669c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -108,11 +108,14 @@ type 'id gclause =
 let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
 
 type 'constr induction_clause =
-  ('constr with_bindings induction_arg list * 'constr with_bindings option *
-   (intro_pattern_expr located option * intro_pattern_expr located option))
+    'constr with_bindings induction_arg *
+    (intro_pattern_expr located option (* eqn:... *)
+    * intro_pattern_expr located option) (* as ... *)
 
 type ('constr,'id) induction_clause_list =
-    'constr induction_clause list * 'id gclause option
+    'constr induction_clause list
+    * 'constr with_bindings option (* using ... *)
+    * 'id gclause option (* in ... *)
 
 type multi =
   | Precisely of int
@@ -160,7 +163,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacAssert of 'tac option * intro_pattern_expr located option * 'constr
   | TacGeneralize of ('constr with_occurrences * name) list
   | TacGeneralizeDep of 'constr
-  | TacLetTac of name * 'constr * 'id gclause * letin_flag
+  | TacLetTac of name * 'constr * 'id gclause * letin_flag *
+      intro_pattern_expr located option
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 08800902..b2a853d7 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 402002de..ef4c7957 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index b23f361c..b56cb844 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 62c2359b..04b3cedf 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3