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=8d852367b54f095d9fbabd000304d450

sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

Sourceval simple_extraction : Libnames.qualid -> unit

Sourceval full_extraction : string option -> Libnames.qualid list -> unit

Sourceval separate_extraction : Libnames.qualid list -> unit

Sourceval extraction_library : bool -> Names.lident -> unit

Sourceval extract_and_compile : Libnames.qualid list -> unit

val mono_environment : 
  Names.GlobRef.t list ->
  Names.ModPath.t list ->
  Miniml.ml_structure

val print_one_decl : 
  Miniml.ml_structure ->
  Names.ModPath.t ->
  Miniml.ml_decl ->
  Pp.t

val structure_for_compute : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type

Sourceval show_extraction : pstate:Declare.Proof.t -> unit