package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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

Module ClenvSource

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
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)

Sourceval mk_clenv_from_n : Environ.env -> Evd.evar_map -> int -> (EConstr.constr * EConstr.types) -> clausenv
linking of clenvs
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

Sourceval 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

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

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

Clenv tactics
Sourceval res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> clausenv -> unit Proofview.tactic
Sourceval 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