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, 483 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