diff options
| author | Pierre-Marie Pédrot | 2015-04-13 08:48:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-13 08:48:20 +0200 |
| commit | 914095183c54a35909c5c31b376e816859a594aa (patch) | |
| tree | 88bb79d32ea7ccbfebfb44994179c5ea94fda694 /plugins | |
| parent | 91172e9c3a1430c3be3ad1080d2da68b25d940aa (diff) | |
Fixing bug #4186.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrOcamlNatInt.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 5f653ee109..a0930f15f4 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -59,6 +59,7 @@ Extract Constant Compare_dec.nat_compare => "fun n m -> if n=m then Eq else if n<m then Lt else Gt". Extract Inlined Constant Compare_dec.leb => "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". +Extract Inlined Constant Compare_dec.lt_dec => "(<)". Extract Constant Compare_dec.lt_eq_lt_dec => "fun n m -> if n>m then None else Some (n<m)". |