diff --git a/README.md b/README.md
index 0c90f604ed00abaf0bfe9ddc9d1b8ea291f9b836..435f995f24603b2b440e225bdcaa87736b053a95 100644
--- a/README.md
+++ b/README.md
@@ -34,6 +34,12 @@ First, create an appropriate `Makefile`.
 ./create_makefile.sh
 ```
 
+Alternatively, to avoid compiling the older "classic" Prosa, specify the `--without-classic` option.
+
+```
+./create_makefile.sh --without-classic
+```
+
 Second, compile the library.
 
 ```
diff --git a/create_makefile.sh b/create_makefile.sh
index 95eba04295ad789cca5b2fdf32e3dda0d3419084..46c35de0c3928a9c2ea46ddce02dc52c42e49eb2 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -1,11 +1,30 @@
 #!/bin/bash 
 
+while ! [ -z "$1" ]
+do
+    case "$1" in
+        --without-classic)
+            SKIP_CLASSIC=yes
+            ;;
+        *)
+            echo "Unrecognized option: $1"
+            exit 1
+            ;;
+    esac
+    shift
+done
+
 # Include rt-proofs library in _CoqProject.
 # (For Coq versions >= 8.6, remove spurious warnings.)
 echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
 
 # Compile all *.v files
-coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -path "./.git/*" -print) -o Makefile
+if [ "yes" == "$SKIP_CLASSIC" ]
+then
+    coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -path "./.git/*" ! -path "./classic/*" -print) -o Makefile
+else
+    coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -path "./.git/*" -print) -o Makefile
+fi
 
 # Fix the 'make validate' command. It doesn't handle the library prefix properly
 # and cause clashes for files with the same name. This forces full filenames and