package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val get_pattern_id : Glob_term.cases_pattern -> Names.Id.t list
val mkGHole : unit -> Glob_term.glob_constr
val is_free_in : Names.Id.t -> Glob_term.glob_constr -> bool
val are_unifiable : Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool
val eq_cases_pattern : Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool
val resolve_and_replace_implicits : ?flags:Pretyping.inference_flags -> ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Glob_term.glob_constr