From 7208928de37565a9e38f9540f2bfb1e7a3b877e6 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 17 Sep 2012 20:46:20 +0000
Subject: More cleaning on Utils and CList. Some parts of the code being
 peculiarly messy, I hope I did not introduce too many bugs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/romega/refl_omega.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 6c6e2c57f2..c6256b0c50 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -929,10 +929,10 @@ let filter_compatible_systems required systems =
   let rec select = function
       (x::l) ->
 	if List.mem x required then select l
-	else if List.mem (barre x) required then failwith "Exit"
+	else if List.mem (barre x) required then raise Exit
 	else x :: select l
     | [] -> [] in
-  map_succeed (function (sol,splits) -> (sol,select splits)) systems
+  List.map_filter (function (sol, splits) -> try Some (sol, select splits) with Exit -> None) systems
 
 let rec equas_of_solution_tree = function
     Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
-- 
cgit v1.2.3