From 5c0f5b7d8af44bfed1d0bad9d0afc2a56f4afa00 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 6 Mar 2018 16:13:12 +0000 Subject: [stdlib] Do not use deprecated notations --- plugins/extraction/ExtrOcamlNatBigInt.v | 2 +- plugins/extraction/ExtrOcamlNatInt.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 264b48a08..c403f7c5a 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -46,7 +46,7 @@ Extract Constant EqNat.eq_nat_decide => "Big.eq". Extract Constant Peano_dec.eq_nat_dec => "Big.eq". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "Big.compare_case Eq Lt Gt". Extract Constant Compare_dec.leb => "Big.le". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 35af71417..a2f809a0c 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -59,7 +59,7 @@ Extract Inlined Constant EqNat.eq_nat_decide => "(=)". Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "fun n m -> if n=m then Eq else if n "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". -- cgit v1.2.3