package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __coq_plugin_name : string
val ground_depth : unit -> int
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 firstorder_using : Libnames.qualid list Pcoq.Entry.t