Module `Evd.MiniEConstr`Source

Use this module only to bootstrap EConstr

Sourcemodule ERelevance : sig ... end

Sourcemodule ESorts : sig ... end

Sourcemodule EInstance : sig ... end

Sourcetype t = econstr

val kind : 
  evar_map ->
  t ->
  (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term

Source

val kind_upto : 
  evar_map ->
  Constr.constr ->
  (Constr.constr, Constr.types, Sorts.t, UVars.Instance.t, Sorts.relevance)
    Constr.kind_of_term

Sourceval whd_evar : evar_map -> t -> t

Sourceval mkLEvar : evar_map -> (Evar.t * t list) -> t

Sourceval replace_vars : evar_map -> (Names.Id.t * t) list -> t -> t

Source

val of_kind : 
  (t, t, ESorts.t, EInstance.t, ERelevance.t) Constr.kind_of_term ->
  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 nf_evar : evar_map -> t -> t

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

Sourceval unsafe_relevance_eq : (ERelevance.t, Sorts.relevance) Util.eq

Source

val of_named_decl : 
  (Constr.t, Constr.types, Sorts.relevance) Context.Named.Declaration.pt ->
  (t, t, ERelevance.t) Context.Named.Declaration.pt

Source

val unsafe_to_named_decl : 
  (t, t, ERelevance.t) Context.Named.Declaration.pt ->
  (Constr.t, Constr.types, Sorts.relevance) Context.Named.Declaration.pt

Source

val unsafe_to_rel_decl : 
  (t, t, ERelevance.t) Context.Rel.Declaration.pt ->
  (Constr.t, Constr.types, Sorts.relevance) Context.Rel.Declaration.pt

Source

val of_case_invert : 
  Constr.constr Constr.pcase_invert ->
  econstr Constr.pcase_invert

Source

val unsafe_to_case_invert : 
  econstr Constr.pcase_invert ->
  Constr.constr Constr.pcase_invert

Source

val of_rel_decl : 
  (Constr.t, Constr.types, Sorts.relevance) Context.Rel.Declaration.pt ->
  (t, t, ERelevance.t) Context.Rel.Declaration.pt

Source

val of_named_context : 
  (Constr.t, Constr.types, Sorts.relevance) Context.Named.pt ->
  (t, t, ERelevance.t) Context.Named.pt

Source

val of_rel_context : 
  (Constr.t, Constr.types, Sorts.relevance) Context.Rel.pt ->
  (t, t, ERelevance.t) Context.Rel.pt

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.engine/Evd/MiniEConstr/index.html

Module `Evd.MiniEConstr`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.engine/Evd/MiniEConstr/index.html

Module Evd.MiniEConstrSource

Module `Evd.MiniEConstr`Source