Module `Ssrsearch_plugin.G_search`Source

Sourceval __coq_plugin_name : string

module CoqConstr = Constr

Sourcetype raw_glob_search_about_item =

| RGlobSearchSubPattern of Constrexpr.constr_expr
| RGlobSearchString of Loc.t * string * string option

val pr_search_item : 
  Environ.env ->
  Evd.evar_map ->
  raw_glob_search_about_item ->
  Pp.t

Sourceval wit_ssr_searchitem : raw_glob_search_about_item Genarg.uniform_genarg_type

Source

val pr_ssr_search_item : 
  Environ.env ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  raw_glob_search_about_item ->
  Pp.t

Sourceval is_ident : string -> bool

Sourceval is_ident_part : string -> bool

Source

val interp_search_notation : 
  ?loc:Loc.t ->
  string ->
  Notation.delimiters option ->
  Search.glob_search_item

Source

val wit_ssr_search_item : 
  (raw_glob_search_about_item,
    raw_glob_search_about_item,
    raw_glob_search_about_item)
    Genarg.genarg_type

Sourceval ssr_search_item : raw_glob_search_about_item Pcoq.Entry.t

Source

val pr_ssr_search_arg : 
  Environ.env ->
  Evd.evar_map ->
  'a ->
  'b ->
  'c ->
  (bool * raw_glob_search_about_item) list ->
  Pp.t

Source

val wit_ssr_search_arg : 
  ((bool * raw_glob_search_about_item) list,
    (bool * raw_glob_search_about_item) list,
    (bool * raw_glob_search_about_item) list)
    Genarg.genarg_type

Sourceval ssr_search_arg : (bool * raw_glob_search_about_item) list Pcoq.Entry.t

Source

val splay_search_pattern : 
  int ->
  Pattern.constr_pattern ->
  Names.GlobRef.t * int

Source

val push_rels_assum : 
  (Names.Name.t Context.binder_annot * EConstr.t) list ->
  Environ.env ->
  Environ.env

Source

val coerce_search_pattern_to_sort : 
  Pattern.constr_pattern ->
  bool * Pattern.constr_pattern

Source

val interp_head_pat : 
  Pattern.constr_pattern ->
  bool * (CoqConstr.constr -> bool)

Sourceval all_true : 'a -> bool

Source

val interp_search_about : 
  (bool * Search.glob_search_item) list ->
  (Names.GlobRef.t ->
    Decls.logical_kind option ->
    Environ.env ->
    Constr.constr ->
    bool) ->
  Names.GlobRef.t ->
  Decls.logical_kind option ->
  Environ.env ->
  Constr.constr ->
  bool

Source

val interp_search_arg : 
  (bool * raw_glob_search_about_item) list ->
  Names.GlobRef.t ->
  Decls.logical_kind option ->
  Environ.env ->
  Constr.constr ->
  bool

Sourceval pr_modloc : (bool * Libnames.qualid) -> Pp.t

Sourceval wit_ssrmodloc : (bool * Libnames.qualid) Genarg.uniform_genarg_type

Sourceval pr_ssr_modlocs : 'a -> 'b -> 'c -> (bool * Libnames.qualid) list -> Pp.t

Source

val wit_ssr_modlocs : 
  ((bool * Libnames.qualid) list,
    (bool * Libnames.qualid) list,
    (bool * Libnames.qualid) list)
    Genarg.genarg_type

Sourceval ssr_modlocs : (bool * Libnames.qualid) list Pcoq.Entry.t

Source

val interp_modloc : 
  (bool * Libnames.qualid) list ->
  Names.GlobRef.t ->
  Decls.logical_kind option ->
  Environ.env ->
  Constr.constr ->
  bool

Sourceval ssrdisplaysearch : Names.GlobRef.t -> Environ.env -> Constr.constr -> unit

Sourceval deprecated_search : ?loc:Loc.t -> unit -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssrsearch_plugin/Ssrsearch_plugin/G_search/index.html

Module `Ssrsearch_plugin.G_search`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ssrsearch_plugin/Ssrsearch_plugin/G_search/index.html

Module Ssrsearch_plugin.G_searchSource

Module `Ssrsearch_plugin.G_search`Source