diff options
| author | letouzey | 2007-10-17 23:29:08 +0000 |
|---|---|---|
| committer | letouzey | 2007-10-17 23:29:08 +0000 |
| commit | e82372fe9b5c1a9c56a605c582d4365e6bfcd593 (patch) | |
| tree | e90a8d1ff76d5349dc01fbe683bd1d999feb85fb /lib/util.mli | |
| parent | 350398eaea679b2bf66c93e9ac5e0308349bc959 (diff) | |
Repair Haskell/Scheme extraction in the new extraction backend design:
Unlike prlist_xxxx and prvect, the function prlist is acting lazily,
which is bad for extraction (synchronization with tables). We add and
use a prlist_strict function.
Additionaly:
- cleanup of the preamble printing
- no need for 2-pass printing (/dev/null trick) when the language
isn't ocaml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10233 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 6d6d9c2a85..5e89788b9b 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -255,6 +255,9 @@ val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val nth : int -> std_ppcmds val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +(* unlike all other functions below, [prlist] works lazily. + if a strict behavior is needed, use [prlist_strict] instead. *) +val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val prlist_with_sep : (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds |