From e8ef565dadd110329f806fa3c281055fcd807440 Mon Sep 17 00:00:00 2001
From: lmamane
Date: Fri, 22 Feb 2008 13:39:13 +0000
Subject: Merge with lmamane's private branch:  - New vernac command "Delete" 
 - New vernac command "Undo To"  - Added a few hooks used by new
 contrib/interface  - Beta/incomplete version of dependency generation and
 dumping

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 2 +-
 tactics/tactics.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 24149a98e7..effd6f9afb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1300,7 +1300,7 @@ let solvable_by_tactic env evi (ev,args) src =
       begin
 	try
 	  by (tclCOMPLETE tac);
-	  let _,(const,_,_) = cook_proof () in 
+	  let _,(const,_,_) = cook_proof ignore in 
 	  delete_current_proof (); const.const_entry_body
 	with e when Logic.catchable_exception e -> 
 	  delete_current_proof();
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fa40e16514..6119185438 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2691,7 +2691,7 @@ let abstract_subproof name tac gl =
       let _,(const,kind,_) =
 	try
 	  by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
-	  let r = cook_proof () in 
+	  let r = cook_proof ignore in 
 	    delete_current_proof (); r
 	with 
 	    e ->
-- 
cgit v1.2.3