diff options
Diffstat (limited to 'examples/Example.v')
| -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. |