package coq

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_r
    CAst.t

Source

val set_default_solver : 
  Vernacexpr.locality_flag ->
  Ltac_plugin.Tacexpr.glob_tactic_expr ->
  unit

Sourceval default_solver : unit -> Vernacexpr.locality_flag * unit Proofview.tactic

Sourceval print_default_solver : unit -> Pp.t

Source

val gen_ground_tac : 
  bool ->
  unit Proofview.tactic option ->
  Names.GlobRef.t list ->
  Hints.hint_db_name list ->
  unit Proofview.tactic

Sourceval pr_firstorder_using_raw : 'a -> 'b -> 'c -> Libnames.qualid list -> Pp.t

Source

val pr_firstorder_using_glob : 
  'a ->
  'b ->
  'c ->
  ('d * Names.GlobRef.t) Locus.or_var list ->
  Pp.t

Sourceval pr_firstorder_using_typed : 'a -> 'b -> 'c -> Names.GlobRef.t list -> Pp.t

Source

val wit_firstorder_using : 
  (Libnames.qualid list,
    Names.GlobRef.t Loc.located Locus.or_var list,
    Names.GlobRef.t list)
    Genarg.genarg_type

Sourceval firstorder_using : Libnames.qualid list Pcoq.Entry.t

package coq

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/firstorder_plugin/Firstorder_plugin/G_ground/index.html

Module Firstorder_plugin.G_groundSource

dune-project
Dependency

Module `Firstorder_plugin.G_ground`Source