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_nf_meta : clausenv -> EConstr.constr -> EConstr.constr
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_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv
val mk_clenv_from_env : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.types) -> clausenv
val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
val clenv_fchain : ?with_univs:bool -> ?flags:Unification.unify_flags -> Constr.metavariable -> clausenv -> clausenv -> clausenv
val old_clenv_unique_resolver : ?flags:Unification.unify_flags -> clausenv -> Goal.goal Evd.sigma -> clausenv
val clenv_unique_resolver : ?flags:Unification.unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
val clenv_dependent : clausenv -> Constr.metavariable list
val clenv_pose_metas_as_evars : clausenv -> Constr.metavariable list -> 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_env_apply : Environ.env -> Evd.evar_map -> int option -> (EConstr.constr * EConstr.constr) -> EConstr.constr Tactypes.bindings -> 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 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