Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_replace)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4561 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 31 insertions, 3 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7f8e74862..d8dc585f3 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -108,7 +108,7 @@ let get_current_proof_name () =
     | Some(na,_,_) -> na
 
 let add_proof (na,pfs,ts) =
-  Edit.create proof_edits (na,pfs,ts,Some (!undo_limit+1))
+  Edit.create proof_edits (na,pfs,ts,!undo_limit+1)
 
 let delete_proof_gen = Edit.delete proof_edits
 
@@ -306,5 +306,28 @@ let reset_top_of_tree () =
   let pts = get_pftreestate () in 
   if not (is_top_pftreestate pts) then mutate top_of_tree
 
-
-
+(** Printers *)
+
+let pr_subgoals_of_pfts pfts = 
+  let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
+  let sigma = project (top_goal_of_pftreestate pfts) in
+  pr_subgoals_existential sigma gls
+
+let pr_open_subgoals () =
+  let pfts = get_pftreestate () in
+  match focus() with
+    | 0 -> 
+	pr_subgoals_of_pfts pfts
+    | n -> 
+	let pf = proof_of_pftreestate pfts in
+	let gls = fst (frontier pf) in 
+	assert (n > List.length gls);
+	if List.length gls < 2 then 
+	  pr_subgoal n gls
+	else 
+	  v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
+	  pr_subgoal n gls)
+
+let pr_nth_open_subgoal n =
+  let pf = proof_of_pftreestate (get_pftreestate ()) in
+  pr_subgoal n (fst (frontier pf))
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f4cc32a55..875a41cd9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -176,3 +176,8 @@ val traverse_prev_unproven : unit -> unit
    proof and goal management, as it is done, for instance in pcoq *)
 val traverse_to : int list -> unit
 val mutate : (pftreestate -> pftreestate) -> unit
+
+(** Printers *)
+
+val pr_open_subgoals    : unit -> std_ppcmds
+val pr_nth_open_subgoal : int -> std_ppcmds