diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/ExtrOcamlNatBigInt.v | 2 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOcamlNatInt.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 3f8e84ecda..0a303b63fc 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -36,7 +36,7 @@ Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)". Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)". Extract Constant max => "Big.max". Extract Constant min => "Big.min". -Extract Constant nat_beq => "Big.eq". +(*Extract Constant nat_beq => "Big.eq".*) Extract Constant EqNat.beq_nat => "Big.eq". Extract Constant EqNat.eq_nat_decide => "Big.eq". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index f69fca984a..a0cb26b5d3 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -45,7 +45,7 @@ Extract Constant minus => "fun n m -> max 0 (n-m)". Extract Constant mult => "( * )". Extract Inlined Constant max => max. Extract Inlined Constant min => min. -Extract Inlined Constant nat_beq => "(=)". +(*Extract Inlined Constant nat_beq => "(=)".*) Extract Inlined Constant EqNat.beq_nat => "(=)". Extract Inlined Constant EqNat.eq_nat_decide => "(=)". @@ -72,4 +72,4 @@ Definition test n m (H:m>0) := nat_compare n (q*m+r). Recursive Extraction test fact. -*)
\ No newline at end of file +*) |