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, 20 insertions, 0 deletions

diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
new file mode 100644
index 000000000..6cdbdd13f
--- /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.