aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/parser
diff options
context:
space:
mode:
authorGravatar bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-06 08:00:30 +0000
committerGravatar bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-06 08:00:30 +0000
commit35be04a48545ccc4e89057943863bf1397f38634 (patch)
tree02789b5f06859d0576ad99c68e4197d883c43dcd /test-suite/parser
parentfa804d0b23431279089066a87b5e70ed6dd93443 (diff)
the output the parser should produce now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5438 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/parser')
-rw-r--r--test-suite/parser/obj_magic.out124
1 files changed, 86 insertions, 38 deletions
diff --git a/test-suite/parser/obj_magic.out b/test-suite/parser/obj_magic.out
index bb0d67265..edd1e751b 100644
--- a/test-suite/parser/obj_magic.out
+++ b/test-suite/parser/obj_magic.out
@@ -12,53 +12,50 @@ a
vernac$ident
H
n
+vernac$none
+0
+n
vernac$id_list
0
n
vernac$inversion
-3
+4
+n
+vernac$none
+0
n
vernac$solve
-2
+3
a
vernac$int
1
a
-vernac$ident
-Ex
+vernac$string
+exists _ : _ , _
a
vernac$ident
a
-n
-vernac$id_opt_ne_list
-1
a
vernac$ident
b
-n
-vernac$binder
-2
-n
-vernac$binder_ne_list
-1
a
vernac$ident
c
n
-vernac$lambdac
-2
-n
-vernac$formula_ne_list
-1
+vernac$formula_list
+3
n
-vernac$appc
+vernac$notation
2
n
vernac$absurd
1
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -69,14 +66,17 @@ n
vernac$discriminate_eq
1
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
a
vernac$ident
-DEq
+deq
a
vernac$ident
H
@@ -87,8 +87,11 @@ n
vernac$simple_user_tac
2
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -99,8 +102,11 @@ n
vernac$injection_eq
1
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -114,8 +120,11 @@ n
vernac$replace_with
2
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -141,8 +150,11 @@ n
vernac$rewrite_rl
3
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -168,8 +180,11 @@ n
vernac$rewrite_rl
3
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -201,8 +216,11 @@ n
vernac$condrewrite_lr
4
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -234,8 +252,11 @@ n
vernac$condrewrite_lr
4
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -246,8 +267,11 @@ n
vernac$deprewrite_lr
1
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -273,8 +297,11 @@ n
vernac$cutrewrite_lr
2
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -294,8 +321,11 @@ n
vernac$eauto_with
3
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -324,8 +354,11 @@ n
vernac$prolog
2
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -357,8 +390,11 @@ n
vernac$eapply
2
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -384,8 +420,11 @@ n
vernac$use_inversion
3
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -417,8 +456,11 @@ n
vernac$use_inversion
3
n
+vernac$none
+0
+n
vernac$solve
-2
+3
a
vernac$int
1
@@ -435,8 +477,11 @@ n
vernac$ring
1
n
+vernac$none
+0
+n
vernac$solve
-2
+3
n
vernac$lr
0
@@ -459,9 +504,12 @@ a
vernac$ident
v
n
-vernac$idtac
+vernac$none
0
n
+vernac$idtac
+1
+n
vernac$hintrewrite
4
n