diff options
| author | letouzey | 2008-03-21 15:53:23 +0000 |
|---|---|---|
| committer | letouzey | 2008-03-21 15:53:23 +0000 |
| commit | 78e8a11a5f40c5ee1c09e279350ab208c4a31b64 (patch) | |
| tree | 2e99dd9fcce4c29a129248350c4bfcd67b163ca3 /interp/implicit_quantifiers.ml | |
| parent | e41d7212c8c768f21a2baf61bb174a57bb7438a1 (diff) | |
Some "if then else" instead of orb and andb, in order to vm_compute lazily
Extraction is unchanged, since orb/andb are detected as un-strict
functions and inlined. This only prevents the use of some potential
clever Extract Inlined Constant andb => "(&&)" and idem for orb, but
this isn't a big deal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10705 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions