summaryrefslogtreecommitdiff
path: root/parsing/highparsing.mllib
blob: 3eb27abbb6cfbf590bc246b99bf8418ac7b8b76a (plain)
1
2
3
4
5
6
7
G_constr
G_vernac
G_prim
G_proofs
G_tactic
G_ltac
G_decl_mode