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

4 files changed, 22 insertions, 4 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c6cb86dc92..81216d1697 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -204,13 +204,14 @@ let current_proof_depth() =
 let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
 
-let cook_proof () =
+let cook_proof k =
   let (pfs,ts) = get_state() 
   and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in
   !xml_cook_proof (strength,pfs);
+  k pfs;
   (ident,
    ({ const_entry_body = pfterm;
       const_entry_type = Some concl;
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index c3d531c692..5de956d465 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -103,7 +103,7 @@ val suspend_proof : unit -> unit
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed *)
 
-val cook_proof : unit -> 
+val cook_proof : (Refiner.pftreestate -> unit) -> 
   identifier * (Entries.definition_entry * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7010153bad..85f8a4f0e0 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
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index e79534b38f..af9da961ba 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -48,6 +48,8 @@ val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
 
 
+(* Install a hook frontier_map and frontier_mapi call on the new node they create *)
+val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit
 (* [frontier_map f n p] applies f on the n-th open subgoal of p and
    rebuilds proof-tree.
    n=1 for first goal, n negative counts from the right *)