Module `Clenv`Source

This file defines clausenv, which is a deprecated way to handle open terms in the proof engine. This API is legacy.

The Type of Constructions clausale environments.

Sourcetype clausenv

Sourceval clenv_evd : clausenv -> Evd.evar_map

Sourceval update_clenv_evd : clausenv -> Evd.evar_map -> clausenv

Sourceval clenv_strip_proj_params : clausenv -> clausenv

val clenv_refresh : 
  Environ.env ->
  Evd.evar_map ->
  Univ.ContextSet.t option ->
  clausenv ->
  clausenv

Sourceval clenv_arguments : clausenv -> Constr.metavariable list

Sourceval clenv_value : clausenv -> EConstr.constr

subject of clenv (instantiated)

Sourceval clenv_type : clausenv -> EConstr.types

type of clenv (instantiated)

Source

val mk_clenv_from : 
  Environ.env ->
  Evd.evar_map ->
  (EConstr.constr * EConstr.types) ->
  clausenv

Source

val mk_clenv_from_n : 
  Environ.env ->
  Evd.evar_map ->
  int ->
  (EConstr.constr * EConstr.types) ->
  clausenv

linking of clenvs

Source

val clenv_instantiate : 
  ?flags:Unification.unify_flags ->
  ?submetas:(Constr.metavariable * Evd.clbinding) list ->
  Constr.metavariable ->
  clausenv ->
  (EConstr.constr * EConstr.types) ->
  clausenv

Unification with clenvs

Source

val clenv_unify_meta_type : 
  ?flags:Unification.unify_flags ->
  Evd.conv_pb ->
  EConstr.constr ->
  Constr.metavariable ->
  clausenv ->
  clausenv

Unifies the type of a meta with a term.

Bindings

Sourceval clenv_independent : clausenv -> Constr.metavariable list

bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to start from the rightmost argument of the template.

Sourceval clenv_missing : clausenv -> Constr.metavariable list

start with a clenv to refine with a given term with bindings

Source

val make_clenv_binding_apply : 
  Environ.env ->
  Evd.evar_map ->
  int option ->
  (EConstr.constr * EConstr.constr) ->
  EConstr.constr Tactypes.bindings ->
  clausenv

the arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None

Source

val make_clenv_binding : 
  Environ.env ->
  Evd.evar_map ->
  (EConstr.constr * EConstr.constr) ->
  EConstr.constr Tactypes.bindings ->
  clausenv

Source

val clenv_push_prod : 
  clausenv ->
  (Constr.metavariable * bool * clausenv) option

if the clause is a product, add an extra meta for this product

Clenv tactics

Source

val unify : 
  ?flags:Unification.unify_flags ->
  EConstr.constr ->
  unit Proofview.tactic

Source

val res_pf : 
  ?with_evars:bool ->
  ?with_classes:bool ->
  ?flags:Unification.unify_flags ->
  clausenv ->
  unit Proofview.tactic

Source

val case_pf : 
  ?with_evars:bool ->
  dep:bool ->
  (EConstr.constr * EConstr.types) ->
  unit Proofview.tactic

Sourceval clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv

Sourceval pr_clenv : clausenv -> Pp.t

Pretty-print (debug only)

Sourcemodule Internal : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.proofs/Clenv/index.html

Module `Clenv`Source

The Type of Constructions clausale environments.

linking of clenvs

Unification with clenvs

Bindings

Clenv tactics

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.proofs/Clenv/index.html

Module ClenvSource

The Type of Constructions clausale environments.

linking of clenvs

Unification with clenvs

Bindings

Clenv tactics

Module `Clenv`Source