diff options
Diffstat (limited to 'plugins/extraction/ExtrOcamlBasic.v')
| -rw-r--r-- | plugins/extraction/ExtrOcamlBasic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 36bb1148b6..02da168fd0 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -(** Restore lazyness of andb, orb. +(** Restore laziness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined - by extraction in order to have lazyness, producing inelegant + by extraction in order to have laziness, producing inelegant (if ... then ... else false) and (if ... then true else ...). *) |