correcting the treatment of many tactics that use quant_hyp in file xlate.ml

and associated file.  Also adding a systematic check approach


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

1 files changed, 22 insertions, 1 deletions

diff --git a/test-suite/check b/test-suite/check
index 3e8a080384..68ef6efd97 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -62,6 +62,26 @@ test_output() {
     done
 }
 
+# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
+# Elle fonctionne comme test_output
+test_parser() {
+    for f in $1/*.v; do
+        nbtests=`expr $nbtests + 1`
+        printf "    "$f"..."
+        tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
+        foutput=`dirname $f`/`basename $f .v`.out
+        echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
+        perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
+            $tmpoutput | diff - $foutput > /dev/null
+        if [ $? = 0 ] ; then
+            echo "Ok"
+            nbtestsok=`expr $nbtestsok + 1`
+        else
+            echo "Error! (unexpected output)"
+        fi
+    done
+}
+
 # Programme principal
 
 echo "Output tests"
@@ -70,7 +90,8 @@ echo "Success tests"
 test_succes success
 echo "Failure tests"
 test_echec failure
-
+echo "Parser tests"
+test_parser parser
 pourcentage=`expr 100 \* $nbtestsok / $nbtests`
 echo
 echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %"