Skip to content

Commit 643424b

Browse files
committed
Remove test-suite relying on unproven checker
1 parent 5b34d94 commit 643424b

File tree

3 files changed

+0
-179
lines changed

3 files changed

+0
-179
lines changed

test-suite/TypingTests.v

Lines changed: 0 additions & 164 deletions
This file was deleted.

test-suite/_CoqProject

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,11 +35,9 @@ opaque.v
3535
proj.v
3636
run_in_tactic.v
3737
safechecker_test.v
38-
# test_term.v -> loaded in TypingTests.v
3938
tmExistingInstance.v
4039
tmFreshName.v
4140
tmInferInstance.v
42-
TypingTests.v
4341
unfold.v
4442
univ.v
4543
tmVariable.v

test-suite/test_term.v

Lines changed: 0 additions & 13 deletions
This file was deleted.

0 commit comments

Comments
 (0)