Mapcard « custom « test « extraction « contrib - coq - The formal proof system

about summary refs log tree commit diff

path: root/contrib/extraction/test/custom/Mapcard

blob: 78c382267bf59746326585a6e7a662bfe5ca40e2 (plain)

Require Plus.
Extraction NoInline plus_is_one.
Require Addr.
Extraction NoInline ad_double ad_double_plus_un.