Firstorder_plugin.G_ground
val wit_firstorder_using : (Libnames.qualid list, Names.GlobRef.t Loc.located Locus.or_var list, Names.GlobRef.t list) Genarg.genarg_type
val firstorder_using : Libnames.qualid list Pcoq.Entry.t