diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-04-12 14:13:00 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-12 14:13:00 +0200 |
| commit | 02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b (patch) | |
| tree | ec18dc8768ea8ca45ed380ffda289fe204a822a5 /unit-tests | |
| parent | ad491f845f6fb3e88ff1169ac472f194d12306d2 (diff) | |
| download | smtcoq-02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b.tar.gz smtcoq-02544aa0e9f2693de4b02a87d8e66cc8e72e3c8b.zip | |
Error message to state that tactics are not supported with native-coq (#47)
* Better error message for failing tactics with native-coq
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 002854c..8b83295 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -1281,7 +1281,7 @@ Section list. Lemma coqhammer_example l1 l2 x y1 y2 y3: implb (orb (inlist x l1) (orb (inlist x l2) (orb (x =? y1) (inlist x (y2 ::y3::nil))))) (inlist x (y1::(l1 ++ (y2 :: (l2 ++ (y3 :: nil)))))). - Proof. verit. Qed. + Proof. verit_no_check. Qed. Clear_lemmas. End list. |