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

1 files changed, 17 insertions, 2 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7010153ba..85f8a4f0e 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -108,13 +108,23 @@ let rec frontier p =
 		  open_subgoals = and_status (List.map pf_status pfl');
 		  ref = Some(r,pfl')}))
 
+(* TODO LEM: I might have to make sure that these hooks are called
+   only when called from solve_nth_pftreestate; I can build the hook
+   call into the "f", then.
+ *)
+let solve_hook = ref ignore
+let set_solve_hook = (:=) solve_hook
 
 let rec frontier_map_rec f n p =
   if n < 1 || n > p.open_subgoals then p else
   match p.ref with
     | None -> 
         let p' = f p in
-        if Evd.eq_evar_info p'.goal p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then
+	  begin
+	    !solve_hook p';
+	    p'
+	  end
         else 
 	  errorlabstrm "Refiner.frontier_map"
             (str"frontier_map was handed back a ill-formed proof.")
@@ -140,7 +150,11 @@ let rec frontier_mapi_rec f i p =
   match p.ref with
     | None -> 
         let p' = f i p in
-        if Evd.eq_evar_info p'.goal p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then
+	  begin
+	    !solve_hook p';
+	    p'
+	  end
         else 
 	  errorlabstrm "Refiner.frontier_mapi"
             (str"frontier_mapi was handed back a ill-formed proof.")
@@ -849,6 +863,7 @@ let prev_unproven pts =
 let rec top_of_tree pts = 
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
+(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
 let change_rule f pts =
   let mark_top _ pt =
     match pt.ref with