From 4c339d5e9efce992bae3c88598d04250946fcdd2 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 9 Oct 2014 15:57:37 +0200
Subject: Proofview: small optimisation/simplification.

---
 proofs/proofview.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e19236df04..a30175de1a 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -162,8 +162,7 @@ let focus i j sp =
   ( { sp with comb = new_comb } , context )
 
 (* Unfocuses a proofview with respect to a context. *)
-let undefined defs l =
-  Option.List.flatten (List.map (Goal.advance defs) l)
+let undefined defs l = CList.map_filter (Goal.advance defs) l
 let unfocus c sp =
   { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
 
-- 
cgit v1.2.3