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 /theories/Numbers/Integer/TreeMod/ZTreeMod.v | |
| 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 'theories/Numbers/Integer/TreeMod/ZTreeMod.v')
0 files changed, 0 insertions, 0 deletions