diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-05-02 00:41:30 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-05-02 00:41:30 +0200 |
| commit | 663a870b7e20f32b4b20cad6baa865df4058e595 (patch) | |
| tree | ddb46c5e56c3745222272140e0fce61cdd721c1b /examples | |
| parent | fb4e5e5be1cc365e3a2ae1758c385ee0fc51e10a (diff) | |
| download | smtcoq-663a870b7e20f32b4b20cad6baa865df4058e595.tar.gz smtcoq-663a870b7e20f32b4b20cad6baa865df4058e595.zip | |
Example.v: new paths for Coq 8.5
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/examples/Example.v b/examples/Example.v index 9dacc6a..930c4a8 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -1,6 +1,9 @@ -(* "Require Import SMTCoq." is needed to use the SMTCoq program *) +(* [Require Import SMTCoq.] loads the SMTCoq library. + If you are using native-coq instead of Coq 8.5, replace it with: + Require Import SMTCoq. + *) -Require Import SMTCoq. +Require Import SMTCoq.SMTCoq. Require Import Bool. Local Open Scope int63_scope. |