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