Skip to content

Commit

Permalink
[test-suite] close the proof
Browse files Browse the repository at this point in the history
  • Loading branch information
gares committed Aug 25, 2020
1 parent af686af commit 8e78a6d
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions test-suite/output/ssr_error_multiple_intro_after_case.v
@@ -1,3 +1,4 @@
Require Import ssreflect.
Goal forall p : nat * nat , True.
case => x x.
Abort.

0 comments on commit 8e78a6d

Please sign in to comment.