diff --git a/docs/dafny/index.html b/docs/dafny/index.html
index f5208efb..eb56a874 100644
--- a/docs/dafny/index.html
+++ b/docs/dafny/index.html
@@ -1,5 +1,7 @@
 Using the Dafny-VMC library in a Dafny application.
 <br>
+<a href="dafny-doc/index.html">Dafny documentation</a>
+<br>
 <a href="ExamplesFoundational.dfy">Example using the foundational uniform sampler</a>
 <br>
 <a href="ExamplesExternUniform.dfy">Example using the extern uniform sampler</a>
\ No newline at end of file
diff --git a/scripts/gendoc.sh b/scripts/gendoc.sh
index 8ab3f331..311120aa 100755
--- a/scripts/gendoc.sh
+++ b/scripts/gendoc.sh
@@ -14,6 +14,9 @@ then
   exit 1
 fi
 
+echo Generating Dafny documentation...
+$DAFNY doc src/Dafny-VMC.dfy --output docs/dafny/dafny-doc/
+
 echo Generating Java documentation...
 $DAFNY translate java src/Dafny-VMC.dfy 
 cp $DAFNYSOURCE/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/*.java src/Dafny-VMC-java/dafny/