package coq-core

  1. Overview
  2. Docs
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 eq_cases_pattern : Environ.env -> Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool
val ids_of_pat : Glob_term.cases_pattern -> Names.Id.Set.t
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
OCaml

Innovation. Community. Security.