2 files changed, 39 insertions, 0 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 0652f19864..a41bfdd49f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -230,6 +230,44 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
+let rec subtrac l1 l2 =
+  match l1,l2 with
+    | [],l -> l
+    | _,[] -> []
+    | _,(e2::l2') -> 
+      if List.mem e2 l1 then subtrac l1 l2'
+      else e2:: subtrac l1 l2'
+      
+
+(* Execute tac and show the names of hypothesis create by tac in
+   the "as" format. The resulting goals are printed *after* the
+   as-expression, which forces pg to some gymnastic. TODO: Have
+   something similar (better?) in the xml protocol. *)
+let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
+    :Proof_type.goal list Evd.sigma =
+  let oldhyps:Sign.named_context = pf_hyps goal in
+  let rslt:Proof_type.goal list Evd.sigma = tac goal in
+  let {it=gls;sigma=sigma} = rslt in
+  let hyps:Sign.named_context list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in
+  let newhyps =
+    List.map (fun hypl -> subtrac oldhyps hypl)
+      hyps in
+  let emacs_str s =
+    if !Flags.print_emacs then s else "" in
+  let s = 
+    let frst = ref true in
+    List.fold_left
+    (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
+      ^ (List.fold_left
+	   (fun acc (nm,_,_) -> (Names.string_of_id nm) ^ " " ^ acc)
+	   "" lh))
+    "" newhyps in
+  pp (str (emacs_str "<infoH>")
+      ++  (hov 0 (str s))
+      ++  (str (emacs_str "</infoH>")) ++ fnl());
+  rslt;;
+
+
 let catch_failerror e =
   if catchable_exception e then check_for_interrupt ()
   else match e with
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4e30c9c0b2..b5fc9ee66f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -136,6 +136,7 @@ val tclDO            : int -> tactic -> tactic
 val tclTIMEOUT       : int -> tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
+val tclSHOWHYPS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 
 (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,