aboutsummaryrefslogtreecommitdiffstats
path: root/examples
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2016-09-21 14:53:26 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2016-09-21 14:53:26 +0200
commitfa9d33eea03bb59d55ee4dccf4fecb8b1520e69d (patch)
tree81dae1f1a005058311f8460e24ea769dd69eede5 /examples
parent7a17276943c42c7997389d4782e457f449bd102e (diff)
downloadsmtcoq-fa9d33eea03bb59d55ee4dccf4fecb8b1520e69d.tar.gz
smtcoq-fa9d33eea03bb59d55ee4dccf4fecb8b1520e69d.zip
Typo
Diffstat (limited to 'examples')
-rw-r--r--examples/Example.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/examples/Example.v b/examples/Example.v
index 930c4a8..a37b2da 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -1,4 +1,4 @@
-(* [Require Import SMTCoq.] loads the SMTCoq library.
+(* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library.
If you are using native-coq instead of Coq 8.5, replace it with:
Require Import SMTCoq.
*)