diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-17 20:46:20 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-17 20:46:20 +0000 |
| commit | 7208928de37565a9e38f9540f2bfb1e7a3b877e6 (patch) | |
| tree | 7d51cd24c406d349f4b7410c81ee66c210df49cd /plugins/romega | |
| parent | a6dac9962929d724c08c9a74a8e05de06469a1a0 (diff) | |
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
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 6c6e2c57f..c6256b0c5 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) |