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

2 files changed, 21 insertions, 17 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index b3fdd384a8..880d4b8ce1 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
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 8fef987e6a..3a0840a7e1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -545,12 +545,15 @@ let rec list_mem_assoc_triple x = function
   | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
 
 let register_empty_levels forpat levels =
-  map_succeed (fun n ->
-    let levels = (if forpat then snd else fst) (List.hd !level_stack) in
-    if not (list_mem_assoc_triple n levels) then
-      find_position_gen forpat true None (Some n)
-    else
-      failwith "") levels
+  let filter n =
+    try
+      let levels = (if forpat then snd else fst) (List.hd !level_stack) in
+      if not (list_mem_assoc_triple n levels) then
+        Some (find_position_gen forpat true None (Some n))
+      else None
+    with Failure _ -> None
+  in
+  List.map_filter filter levels
 
 let find_position forpat assoc level =
   find_position_gen forpat false assoc level