diff options
Diffstat (limited to 'plugins/extraction/ExtrOcamlBasic.v')
| -rw-r--r-- | plugins/extraction/ExtrOcamlBasic.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 1fcdfd655..f01352212 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -10,17 +10,17 @@ Extract Inductive bool => bool [ true false ]. Extract Inductive option => option [ Some None ]. -Extract Inductive prod => "( * )" [ "" ]. - (* The "" above is a hack, but produce nicer code than with "(,)" *) Extract Inductive unit => unit [ "()" ]. Extract Inductive list => list [ "[]" "( :: )" ]. +Extract Inductive prod => "( * )" [ "" ]. -(** We could also map sumbool to bool, sumor to option, but - this isn't always a gain in clarity. We leave it to the user... +(** NB: The "" above is a hack, but produce nicer code than "(,)" *) + +(** Mapping sumbool to bool and sumor to option is not always nicer, + but it helps when realizing stuff like [lt_eq_lt_dec] *) Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -*) (** Restore lazyness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined |