Module `Ground_plugin.G_ground`

val __coq_plugin_name : string
val ground_depth : int Stdlib.ref
val default_intuition_tac : < constant : Ltac_plugin.Tacexpr.g_cst; dterm : Ltac_plugin.Tacexpr.g_trm; level : Genarg.glevel; name : Ltac_plugin.Tacexpr.g_nam; pattern : Ltac_plugin.Tacexpr.g_pat; reference : Ltac_plugin.Tacexpr.g_ref; tacexpr : Ltac_plugin.Tacexpr.glob_tactic_expr; term : Ltac_plugin.Tacexpr.g_trm; > Ltac_plugin.Tacexpr.gen_tactic_expr
val set_default_solver : Vernacexpr.locality_flag -> Ltac_plugin.Tacexpr.glob_tactic_expr -> unit
val default_solver : unit -> Vernacexpr.locality_flag * unit Proofview.tactic
val print_default_solver : unit -> Pp.t
val gen_ground_tac : bool -> unit Proofview.tactic option -> Names.GlobRef.t list -> Hints.hint_db_name list -> unit Proofview.tactic

val pr_firstorder_using_raw : 'a -> 'b -> 'c -> Libnames.qualid list -> Pp.t
val pr_firstorder_using_glob : 'a -> 'b -> 'c -> ('d * Names.GlobRef.t) Locus.or_var list -> Pp.t
val pr_firstorder_using_typed : 'a -> 'b -> 'c -> Names.GlobRef.t list -> Pp.t
val warn_deprecated_syntax : ?⁠loc:Loc.t -> unit -> unit
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