Module Firstorder_plugin.G_ground

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