summaryrefslogtreecommitdiff
path: root/contrib/extraction/test/custom/Map
blob: f024dbd79202d5a1f9a6ed31701b5a24e01977c7 (plain)
1
2
3
Require Import BinNat.
Extraction NoInline Ndouble Ndouble_plus_one.