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