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

3 files changed, 525 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 %"
diff --git a/test-suite/parser/obj_magic.out b/test-suite/parser/obj_magic.out
new file mode 100644
index 0000000000..fef49b8f64
--- /dev/null
+++ b/test-suite/parser/obj_magic.out
@@ -0,0 +1,483 @@
+Starting Centaur Specialized Parser Loop
+message
+parsed
+1
+a
+vernac$int
+1
+n
+vernac$inv_regular
+0
+a
+vernac$ident
+H
+n
+vernac$id_list
+0
+n
+vernac$inversion
+3
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+Ex
+a
+vernac$ident
+a
+n
+vernac$id_opt_ne_list
+1
+a
+vernac$ident
+b
+n
+vernac$binder
+2
+a
+vernac$ident
+c
+n
+vernac$lambdac
+2
+n
+vernac$formula_ne_list
+1
+n
+vernac$appc
+2
+n
+vernac$absurd
+1
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+n
+vernac$discriminate_eq
+1
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+DEq
+a
+vernac$ident
+H
+n
+vernac$tactic_arg_list
+1
+n
+vernac$simple_user_tac
+2
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+n
+vernac$injection_eq
+1
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+a
+a
+vernac$ident
+b
+n
+vernac$replace_with
+2
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+a
+vernac$ident
+a
+a
+vernac$ident
+b
+n
+vernac$binding
+2
+n
+vernac$binding_list
+1
+n
+vernac$none
+0
+n
+vernac$rewrite_rl
+3
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+a
+vernac$ident
+a
+a
+vernac$ident
+b
+n
+vernac$binding
+2
+n
+vernac$binding_list
+1
+a
+vernac$ident
+H1
+n
+vernac$rewrite_rl
+3
+n
+vernac$solve
+2
+a
+vernac$int
+1
+n
+vernac$none
+0
+n
+vernac$auto
+1
+a
+vernac$ident
+H
+a
+vernac$int
+1
+a
+vernac$ident
+b
+n
+vernac$binding
+2
+n
+vernac$binding_list
+1
+n
+vernac$none
+0
+n
+vernac$condrewrite_lr
+4
+n
+vernac$solve
+2
+a
+vernac$int
+1
+n
+vernac$none
+0
+n
+vernac$auto
+1
+a
+vernac$ident
+H
+a
+vernac$int
+1
+a
+vernac$ident
+b
+n
+vernac$binding
+2
+n
+vernac$binding_list
+1
+a
+vernac$ident
+H2
+n
+vernac$condrewrite_lr
+4
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+n
+vernac$deprewrite_lr
+1
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+eq
+n
+vernac$existvarc
+0
+a
+vernac$ident
+a
+a
+vernac$ident
+b
+n
+vernac$formula_ne_list
+3
+n
+vernac$appc
+2
+n
+vernac$none
+0
+n
+vernac$cutrewrite_lr
+2
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$int
+3
+a
+vernac$int
+4
+a
+vernac$ident
+a
+n
+vernac$id_ne_list
+1
+n
+vernac$eauto_with
+3
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+A
+a
+vernac$ident
+B
+a
+vernac$ident
+c
+n
+vernac$formula_ne_list
+1
+n
+vernac$appc
+2
+n
+vernac$formula_list
+2
+a
+vernac$int
+4
+n
+vernac$prolog
+2
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+a
+vernac$int
+1
+a
+vernac$ident
+H2
+n
+vernac$binding
+2
+a
+vernac$ident
+a
+a
+vernac$ident
+b
+n
+vernac$binding
+2
+n
+vernac$binding_list
+2
+n
+vernac$eapply
+2
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+a
+vernac$ident
+A
+a
+vernac$ident
+b
+n
+vernac$formula_ne_list
+1
+n
+vernac$appc
+2
+n
+vernac$id_list
+0
+n
+vernac$use_inversion
+3
+n
+vernac$solve
+2
+a
+vernac$int
+1
+a
+vernac$ident
+H
+a
+vernac$ident
+A
+a
+vernac$ident
+b
+n
+vernac$formula_ne_list
+1
+n
+vernac$appc
+2
+a
+vernac$ident
+H1
+a
+vernac$ident
+H2
+n
+vernac$id_list
+2
+n
+vernac$use_inversion
+3
+n
+vernac$solve
+2
+n
+vernac$lr
+0
+a
+vernac$ident
+A
+a
+vernac$ident
+b
+n
+vernac$formula_ne_list
+1
+n
+vernac$appc
+2
+n
+vernac$formula_ne_list
+1
+a
+vernac$ident
+v
+n
+vernac$idtac
+0
+n
+vernac$hintrewrite
+4
+n
+vernac$rl
+0
+a
+vernac$ident
+A
+a
+vernac$ident
+b
+n
+vernac$formula_ne_list
+1
+n
+vernac$appc
+2
+n
+vernac$formula_ne_list
+1
+a
+vernac$ident
+v
+n
+vernac$none
+0
+n
+vernac$auto
+1
+n
+vernac$hintrewrite
+4
+n
+vernac$command_list
+19
+e
+blabla
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
new file mode 100644
index 0000000000..6cdbdd13f6
--- /dev/null
+++ b/test-suite/parser/obj_magic.v
@@ -0,0 +1,20 @@
+Inversion H.
+Absurd (Ex [a:b] c).
+Discriminate H.
+DEq H.
+Injection H.
+Replace a with b.
+Rewrite <- H with a:=b.
+Rewrite <- H with a:=b in H1.
+Conditional Auto Rewrite H with 1:=b.
+Conditional Auto Rewrite H with 1:=b in H2.
+Dependent Rewrite -> H.
+CutRewrite -> (a=b).
+EAuto 3 4 with a.
+Prolog [A (B c)] 4.
+EApply H with 1:= H2 a:= b.
+Inversion H using (A b).
+Inversion H using (A b) in H1 H2.
+
+Hint Rewrite -> [ (A b) ] in v.
+Hint Rewrite <- [ (A b) ] in v using Auto.