test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo_before.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.
  constructor.
Qed.
Goal True.
  constructor.
Qed.
Goal True.
  constructor.
Qed.
Goal True.
  constructor.
Qed.
Goal True.
  constructor.
Qed.
Goal List.repeat Z.div_eucl 5 = List.repeat Z.div_eucl 5.
  vm_compute; reflexivity.
Qed.