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