Affichage des notations récursives:

- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives 
  sous forme de terme par une représentation directe (permet notamment
  de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 5 deletions

diff --git a/lib/util.ml b/lib/util.ml
index eb096c3cf..d1e24e321 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -730,13 +730,21 @@ let list_subset l1 l2 =
   in 
   look l1
 
-let list_splitby p = 
-  let rec splitby_loop x y = 
+let list_split_at p = 
+  let rec split_at_loop x y = 
     match y with 
       | []      -> ([],[])
-      | (a::l)  -> if (p a) then (x,y) else (splitby_loop (x@[a]) l)
+      | (a::l)  -> if (p a) then (x,y) else (split_at_loop (x@[a]) l)
   in 
-  splitby_loop []
+  split_at_loop []
+
+let list_split_by p = 
+  let rec split_loop = function
+  | []      -> ([],[])
+  | (a::l)  ->
+      let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2)
+  in 
+  split_loop
 
 let rec list_split3 = function
   | [] -> ([], [], [])
diff --git a/lib/util.mli b/lib/util.mli
index 40d6046d7..46fd7b02e 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -146,7 +146,8 @@ val list_uniquize : 'a list -> 'a list
 (* merges two sorted lists and preserves the uniqueness property: *)
 val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
-val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
 val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
 val list_firstn : int -> 'a list -> 'a list