package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

For extracting "module ... with ..." declaration

val extract_with_type : Environ.env -> Evd.evar_map -> EConstr.t -> (Names.Id.t list * Miniml.ml_type) option
val extract_inductive : Environ.env -> Names.MutInd.t -> Miniml.ml_ind

For Extraction Compute and Show Extraction

val logical_decl : Miniml.ml_decl -> bool
val logical_spec : Miniml.ml_spec -> bool