From 0c77c34291ce7d699456b21b07b0ecf2cb366c31 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 2 Oct 2012 15:25:47 +0000
Subject: 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
---
 proofs/refiner.ml | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'proofs')

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 = 
-- 
cgit v1.2.3