From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2

---
 tactics/class_tactics.ml4 | 4 ++--
 tactics/equality.ml       | 6 +++---
 tactics/tactics.ml        | 4 ++--
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index afd13b4c..66f15fbe 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: class_tactics.ml4 13902 2011-03-10 15:50:24Z msozeau $ *)
 
 open Pp
 open Util
@@ -85,7 +85,7 @@ let evars_to_goals p evm =
     if goals = [] then None
     else
       let goals = List.rev goals in
-      let evm' = evars_reset_evd evm' evm in
+      let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in
 	Some (goals, evm')
 
 (** Typeclasses instance search tactic / eauto *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7a774cc9..411ccc0e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *)
+(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *)
 
 open Pp
 open Util
@@ -888,8 +888,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with
 	| Some w ->
             let w_type = type_of env sigma w in
-            if Evarconv.e_conv env evdref w_type a then
-              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+            if Evarconv.e_cumul env evdref w_type a then
+              applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
 	| None -> anomaly "Not enough components to build the dependent tuple"
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 569cf356..771047fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *)
+(* $Id: tactics.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
 
 open Pp
 open Util
@@ -3469,7 +3469,7 @@ let abstract_subproof id tac gl =
     try flush_and_check_evars (project gl) concl
     with Uninstantiated_evar _ ->
       error "\"abstract\" cannot handle existentials." in
-  let const = Pfedit.build_constant_by_tactic secsign concl
+  let const = Pfedit.build_constant_by_tactic id secsign concl
     (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
   let cd = Entries.DefinitionEntry const in
   let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in
-- 
cgit v1.2.3