diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2018-12-03 08:08:56 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2018-12-03 08:08:56 +0100 |
| commit | 36548d6634864a131cc83ce21491c797163de305 (patch) | |
| tree | 283b642e4cdb593ee6add5c4bdeb0ccec1a9258d /examples | |
| parent | 3fdc107b26f475c8fe8b7052de826405b88c14b3 (diff) | |
| download | smtcoq-36548d6634864a131cc83ce21491c797163de305.tar.gz smtcoq-36548d6634864a131cc83ce21491c797163de305.zip | |
verit also works when it doesn't use the conclusion (#24)
Fixes issue #20
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/examples/Example.v b/examples/Example.v index 2141843..0dba915 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -191,7 +191,7 @@ Section mult3. Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3. Add_lemmas mult3_0 mult3_Sn. - Lemma mult3_21 : mult3 7 =? 21. + Lemma mult3_21 : mult3 4 =? 12. Proof. verit. Qed. Clear_lemmas. |