package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type clausenv = {
  1. env : Environ.env;
  2. evd : Evd.evar_map;
  3. templval : EConstr.constr Evd.freelisted;
  4. templtyp : EConstr.constr Evd.freelisted;
}
val clenv_value : clausenv -> EConstr.constr
val clenv_type : clausenv -> EConstr.types
val clenv_meta_type : clausenv -> Constr.metavariable -> EConstr.types
val mk_clenv_from_n : Proofview.Goal.t -> int option -> (EConstr.constr * EConstr.types) -> clausenv
val mk_clenv_from_env : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.types) -> clausenv
val clenv_fchain : ?with_univs:bool -> ?flags:Unification.unify_flags -> Constr.metavariable -> clausenv -> clausenv -> clausenv
val clenv_independent : clausenv -> Constr.metavariable list
val clenv_missing : clausenv -> Constr.metavariable list
exception NoSuchBinding
val clenv_constrain_last_binding : EConstr.constr -> clausenv -> clausenv
val clenv_unify_meta_types : ?flags:Unification.unify_flags -> clausenv -> clausenv
val make_clenv_binding_apply : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> clausenv
exception NotExtensibleClause
val clenv_push_prod : clausenv -> clausenv
val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:Unification.unify_flags -> clausenv -> unit Proofview.tactic
val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
val pr_clenv : clausenv -> Pp.t
type hole = {
  1. hole_evar : EConstr.constr;
  2. hole_type : EConstr.types;
  3. hole_deps : bool;
  4. hole_name : Names.Name.t;
}
type clause = {
  1. cl_holes : hole list;
  2. cl_concl : EConstr.types;
}
val make_evar_clause : Environ.env -> Evd.evar_map -> ?len:int -> EConstr.types -> Evd.evar_map * clause
val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Tactypes.bindings -> Evd.evar_map
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct