diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 18:08:53 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-27 18:29:50 +0200 |
| commit | 4e6129afb9aab53d14f16ac74a5a4e80323b5813 (patch) | |
| tree | 7037708e3ae50407842b8216117d0edb47e71c60 /examples | |
| parent | a2e8b2f68fa82ca96468cb0613710c07b27192da (diff) | |
| download | smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.tar.gz smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.zip | |
formatting
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/examples/Example.v b/examples/Example.v index fe00931..0c50909 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -58,7 +58,6 @@ Proof. verit. Qed. - Goal forall b1 b2 x1 x2, implb (ifb b1 @@ -69,7 +68,6 @@ Proof. verit. Qed. - (* Examples of using the conversion tactics *) Local Open Scope positive_scope. @@ -137,4 +135,4 @@ nat_convert. verit. Qed. -Local Close Scope nat_scope.
\ No newline at end of file +Local Close Scope nat_scope. |