Add new directory for pre-compilation of files needed for further tests.

Application to the test of notation import from within a section.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11652 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 25 insertions, 0 deletions

diff --git a/test-suite/check b/test-suite/check
index 47960e98d..68a4b0e38 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -9,6 +9,7 @@ else
 fi
 
 command="$coqtop -top Top -load-vernac-source"
+coqc="$coqtop -compile"
 
 # on compte le nombre de tests et de succès
 nbtests=0
@@ -234,8 +235,24 @@ test_features () {
     done
 }
 
+# Compile in advance files needed for tests involving a "Require"
+prepare_tests () {
+    files=`/bin/ls -1 $1/*.v 2> /dev/null`
+    for f in $files; do 
+	printf "    "$f"..."
+	$coqc $1/`basename $f .v` > /dev/null 2>&1 
+	if [ $? != 0 ]; then
+	    echo "could not be prepared"
+        else 
+	    echo "correctly prepared"
+        fi
+    done
+}
+
 # Programme principal
 
+echo "Preparing tests"
+prepare_tests prerequisite
 echo "Success tests"
 test_success success
 echo "Failure tests"
diff --git a/test-suite/prerequisite/make_notation.v b/test-suite/prerequisite/make_notation.v
new file mode 100644
index 000000000..4a75713d1
--- /dev/null
+++ b/test-suite/prerequisite/make_notation.v
@@ -0,0 +1,3 @@
+(* Used in Notation.v to test import of notations from files in sections *)
+
+Notation "'Z'" := O (at level 9).
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 6dce0401d..63f85bc70 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -26,3 +26,8 @@ Notation "x +1" := (S x) (at level 8, right associativity).
    right order *)
 
 Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
+
+(* Check import of notations from within a section *)
+
+Notation "+1 x" := (S x) (at level 25, x at level 9).
+Section A. Notation Global "'Z'" := O (at level 9). End A.