Starting Centaur Specialized Parser Loop
message
parsed
1
a
vernac$int
1
n
vernac$inv_regular
0
a
vernac$ident
H
n
vernac$none
0
n
vernac$id_list
0
n
vernac$inversion
4
n
vernac$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$string
exists _ : _ , _
a
vernac$ident
a
a
vernac$ident
b
a
vernac$ident
c
n
vernac$formula_list
3
n
vernac$notation
2
n
vernac$absurd
1
n
vernac$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$ident
H
n
vernac$discriminate_eq
1
n
vernac$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$ident
H
n
vernac$injection_eq
1
n
vernac$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$ident
a
a
vernac$ident
b
n
vernac$replace_with
2
n
vernac$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$ident
H
n
vernac$deprewrite_lr
1
n
vernac$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$string
_ = _
a
vernac$ident
a
a
vernac$ident
b
n
vernac$formula_list
2
n
vernac$notation
2
n
vernac$none
0
n
vernac$cutrewrite_lr
2
n
vernac$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
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$none
0
n
vernac$solve
3
a
vernac$int
1
a
vernac$ident
a
a
vernac$ident
b
n
vernac$formula_list
2
n
vernac$ring
1
n
vernac$none
0
n
vernac$solve
3
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$none
0
n
vernac$idtac
1
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
20
e
blabla