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

1 files changed, 12 insertions, 11 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index b3fdd384a..880d4b8ce 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -171,12 +171,13 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
   grammar_extend entry reinit (pos,[(name, p4assoc, [])])
 
 let pure_sublevels level symbs =
-  map_succeed
-    (function s ->
-       let i = level_of_snterml s in
-       if level = Some i then failwith "";
-       i)
-    symbs
+  let filter s =
+    try
+      let i = level_of_snterml s in
+      if level = Some i then None else Some i
+    with Failure _ -> None
+  in
+  List.map_filter filter symbs
 
 let extend_constr (entry,level) (n,assoc) mkact forpat rules =
   List.fold_left (fun nb pt ->
@@ -260,11 +261,11 @@ let extend_grammar gram =
   grammar_state := (nb,gram) :: !grammar_state
 
 let recover_notation_grammar ntn prec =
-  let l = map_succeed (function
-    | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
-	 vars, x
-    | _ ->
-	 failwith "") !grammar_state in
+  let filter = function
+  | _, Notation (prec', vars, (_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+    Some (vars, x)
+  | _ -> None in
+  let l = List.map_filter filter !grammar_state in
   assert (List.length l = 1);
   List.hd l