package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

md5=13d2793fc6413aac5168822313e4864e

sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

Sourceval pr_spc : unit -> Pp.t

Sourceval pr_bar : unit -> Pp.t

Sourceval pr_list : (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t

Sourceval pp_concat : Pp.t -> ?sep:Pp.t -> Pp.t list -> Pp.t

Sourceval pr_clear : (unit -> Pp.t) -> Ssrast.ssrclear -> Pp.t

Sourceval pr_clear_ne : Ssrast.ssrclear -> Pp.t

Sourceval pr_dir : Ssrast.ssrdir -> Pp.t

Sourceval pr_simpl : Ssrast.ssrsimpl -> Pp.t

val pr_term : 
  (Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option)) ->
  Pp.t

Sourceval pr_ast_closure_term : Ssrast.ast_closure_term -> Pp.t

Sourceval pr_view2 : Ssrast.ast_closure_term list -> Pp.t

Sourceval pr_ipat : Ssrast.ssripat -> Pp.t

Sourceval pr_ipats : Ssrast.ssripats -> Pp.t

Sourceval pr_iorpat : Ssrast.ssripatss -> Pp.t

Sourceval pr_block : Ssrast.id_block -> Pp.t

Sourceval pr_hyp : Ssrast.ssrhyp -> Pp.t

Sourceval pr_hyps : Ssrast.ssrhyps -> Pp.t

Sourceval prl_constr_expr : Constrexpr.constr_expr -> Pp.t

Sourceval prl_glob_constr : Glob_term.glob_constr -> Pp.t

Sourceval pr_guarded : (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t

Sourceval pr_occ : Ssrast.ssrocc -> Pp.t

Sourceval debug_ssr : CDebug.t