diff options
| author | Pierre-Marie Pédrot | 2015-04-15 09:52:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-15 09:52:13 +0200 |
| commit | 148cf78a4d85ec56818a8ff00719a775670950b9 (patch) | |
| tree | ea4540bb896b3bbedb7c41b80fcf7e0ff1cd04aa /plugins/extraction | |
| parent | 429f493997e34bfaac930c68bf6b267a5b9640ee (diff) | |
| parent | 6f40831dc1d0fecfbaf9fbc8116da0e74b6e8726 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins/extraction')
| -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)". |