test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_after.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal True.
  exact I.
Qed.
Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5.
  vm_compute; reflexivity.
Qed.