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 clenv_meta_list : clausenv -> Unification.Meta.t

val update_clenv_evd : 
  clausenv ->
  Evd.evar_map ->
  Unification.Meta.t ->
  clausenv

Sourceval clenv_strip_proj_params : clausenv -> clausenv

Source

val clenv_refresh : 
  Environ.env ->
  Evd.evar_map ->
  UnivGen.sort_context_set 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 list * Unification.Meta.t) ->
  Constr.metavariable ->
  clausenv ->
  (EConstr.constr * EConstr.types) ->
  clausenv

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 -> Names.Name.t list * int

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 ->
  cv_pb:Conversion.conv_pb ->
  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/rocq-runtime.proofs/Clenv/index.html

Module `Clenv`Source

The Type of Constructions clausale environments.

linking of clenvs

Bindings

Clenv tactics

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.proofs/Clenv/index.html

Module ClenvSource

The Type of Constructions clausale environments.

linking of clenvs

Bindings

Clenv tactics

Module `Clenv`Source