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