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

2 files changed, 503 insertions, 0 deletions

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