package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val cases_pattern_eq : Glob_term.cases_pattern -> Glob_term.cases_pattern -> bool
val cast_type_eq : ('a -> 'a -> bool) -> 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
val glob_constr_eq : Glob_term.glob_constr -> Glob_term.glob_constr -> bool
val cases_pattern_loc : Glob_term.cases_pattern -> Loc.t option
val cases_predicate_names : Glob_term.tomatch_tuples -> Names.Name.t list
val warn_variable_collision : ?loc:Loc.t -> Names.Id.t -> unit
val fold_glob_constr : ('a -> Glob_term.glob_constr -> 'a) -> 'a -> Glob_term.glob_constr -> 'a
val fold_glob_constr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> 'b -> Glob_term.glob_constr -> 'b) -> 'a -> 'b -> Glob_term.glob_constr -> 'b
val iter_glob_constr : (Glob_term.glob_constr -> unit) -> Glob_term.glob_constr -> unit
val occur_glob_constr : Names.Id.t -> Glob_term.glob_constr -> bool
val free_glob_vars : Glob_term.glob_constr -> Names.Id.t list
val bound_glob_vars : Glob_term.glob_constr -> Names.Id.Set.t
val loc_of_glob_constr : Glob_term.glob_constr -> Loc.t option
val glob_visible_short_qualid : Glob_term.glob_constr -> Names.Id.t list
exception UnsoundRenaming
val rename_var : (Names.Id.t * Names.Id.t) list -> Names.Id.t -> Names.Id.t
val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern
val glob_constr_of_closed_cases_pattern : Glob_term.cases_pattern -> Names.Name.t * Glob_term.glob_constr
val add_patterns_for_params_remove_local_defs : Names.constructor -> Glob_term.cases_pattern list -> Glob_term.cases_pattern list
val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
val empty_lvar : Glob_term.ltac_var_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