summaryrefslogtreecommitdiff
path: root/parsing/highparsing.mllib
blob: 8df519b5675ad20270c49d469e277205ddc878b8 (plain)
1
2
3
4
5
G_constr
G_vernac
G_prim
G_proofs
G_tactic