From e03d1840a8e6eec927e7fbe006d59ab21b8d818f Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 22 Oct 2008 11:21:45 +0000 Subject: 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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/util.ml | 16 ++++++++++++---- lib/util.mli | 3 ++- 2 files changed, 14 insertions(+), 5 deletions(-) (limited to 'lib') 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 -- cgit v1.2.3