summaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/timing/per-file-after/A.v
blob: 851e2b9738476c59542d5b53cf1d7c993d667f50 (plain)
1
2
3
4
Require Coq.ZArith.BinInt.
Declare Reduction comp := native_compute.
Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl).
Definition foo1 := Eval comp in (foo0, foo0).