G_constr
G_vernac
G_prim
G_proofs
G_tactic
G_ltac
G_obligations