aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-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.
*)