Skip to content

Commit c9c0046

Browse files
committed
Extra test case
1 parent f2850e6 commit c9c0046

1 file changed

Lines changed: 10 additions & 0 deletions

File tree

tests/util/Errors.v

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,16 @@ Proof.
118118
Assume that (a ⊂ A).
119119
Abort.
120120

121+
Print Grammar waterproof_tactic.
122+
123+
(* Test 19: Misspelling second word after expr *)
124+
Goal (0 = 0) -> True.
125+
Proof.
126+
Assume that (0 = 0) (i).
127+
By (i) it holds tht (1 = 1).
128+
Abort.
129+
130+
121131

122132

123133

0 commit comments

Comments
 (0)