From 914095183c54a35909c5c31b376e816859a594aa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 Apr 2015 08:48:20 +0200
Subject: Fixing bug #4186.

---
 plugins/extraction/ExtrOcamlNatInt.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/extraction')

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)".
 
-- 
cgit v1.2.3