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