package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type glob_search_about_item =
  1. | GlobSearchSubPattern of Pattern.constr_pattern
  2. | GlobSearchString of string
type filter_function = Names.GlobRef.t -> Environ.env -> Constr.constr -> bool
type display_function = Names.GlobRef.t -> Environ.env -> Constr.constr -> unit
val blacklist_filter : filter_function
val module_filter : (Names.DirPath.t list * bool) -> filter_function
val search_about_filter : glob_search_about_item -> filter_function
val search_by_head : int option -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
val search_rewrite : int option -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
val search_pattern : int option -> Pattern.constr_pattern -> (Names.DirPath.t list * bool) -> display_function -> unit
val search_about : int option -> (bool * glob_search_about_item) list -> (Names.DirPath.t list * bool) -> display_function -> unit
type search_constraint =
  1. | Name_Pattern of Str.regexp
  2. | Type_Pattern of Pattern.constr_pattern
  3. | SubType_Pattern of Pattern.constr_pattern
  4. | In_Module of Names.DirPath.t
  5. | Include_Blacklist
type !'a coq_object = {
  1. coq_object_prefix : string list;
  2. coq_object_qualid : string list;
  3. coq_object_object : 'a;
}