summaryrefslogtreecommitdiff
path: root/test-suite/success/extraction.v
blob: e7da947b594c29c0d0efe92971d1d077c5caefc1 (plain) 
1
2
3
4
5

(* Mini extraction test *)

Require Import ZArith.

Extraction "zarith.ml" two_or_two_plus_one Zdiv_eucl_exist.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 15:51:41 +0000