Use the library function List.substract in prev commit

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

1 files changed, 3 insertions, 12 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a41bfdd49f..ac8de601e0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -230,15 +230,6 @@ 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
@@ -248,10 +239,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal 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 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
+    List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
   let emacs_str s =
     if !Flags.print_emacs then s else "" in
   let s =