package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/coq-core.engine/Evd/MiniEConstr/index.html

Module Evd.MiniEConstrSource

Use this module only to bootstrap EConstr

Sourcemodule ESorts : sig ... end
Sourcemodule EInstance : sig ... end
Sourcetype t = econstr
Sourceval whd_evar : evar_map -> t -> t
Sourceval of_constr : Constr.t -> t
Sourceval of_constr_array : Constr.t array -> t array
Sourceval to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
Sourceval to_constr_opt : evar_map -> t -> Constr.t option
Sourceval unsafe_to_constr : t -> Constr.t
Sourceval unsafe_to_constr_array : t array -> Constr.t array
Sourceval unsafe_eq : (t, Constr.t) Util.eq
OCaml

Innovation. Community. Security.