Mapcard « custom « test « extraction « contrib - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: ca555aa32e3480667669ae0a0b206385caa7ef2b (plain)

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