package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
val cases_pattern_eq : 'a Glob_term.cases_pattern_g -> 'a Glob_term.cases_pattern_g -> bool
exception ComplexSort
val glob_sort_family : Glob_term.glob_sort -> Sorts.family
val alias_of_pat : 'a Glob_term.cases_pattern_g -> Names.Name.t
val cast_type_eq : ('a -> 'a -> bool) -> 'a Glob_term.cast_type -> 'a Glob_term.cast_type -> bool
val glob_constr_eq : 'a Glob_term.glob_constr_g -> 'a Glob_term.glob_constr_g -> bool
val map_cast_type : ('a -> 'b) -> 'a Glob_term.cast_type -> 'b Glob_term.cast_type
val smartmap_cast_type : ('a -> 'a) -> 'a Glob_term.cast_type -> 'a Glob_term.cast_type
val cases_pattern_loc : 'a Glob_term.cases_pattern_g -> Loc.t option
val cases_predicate_names : 'a Glob_term.tomatch_tuples_g -> Names.Name.t list
val binding_kind_eq : Glob_term.binding_kind -> Glob_term.binding_kind -> bool
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 -> 'a Glob_term.glob_constr_g -> bool
val free_glob_vars : 'a Glob_term.glob_constr_g -> Names.Id.Set.t
val bound_glob_vars : Glob_term.glob_constr -> Names.Id.Set.t
val loc_of_glob_constr : 'a Glob_term.glob_constr_g -> Loc.t option
val glob_visible_short_qualid : 'a Glob_term.glob_constr_g -> Names.Id.Set.t
exception UnsoundRenaming
val rename_var : (Names.Id.t * Names.Id.t) list -> Names.Id.t -> Names.Id.t
val rename_glob_vars : (Names.Id.t * Names.Id.t) list -> 'a Glob_term.glob_constr_g -> 'a Glob_term.glob_constr_g
val cases_pattern_of_glob_constr : Environ.env -> Names.Name.t -> 'a Glob_term.glob_constr_g -> 'a Glob_term.cases_pattern_g
val glob_constr_of_closed_cases_pattern : Environ.env -> 'a Glob_term.cases_pattern_g -> Names.Name.t * 'a Glob_term.glob_constr_g
val glob_constr_of_cases_pattern : Environ.env -> 'a Glob_term.cases_pattern_g -> 'a Glob_term.glob_constr_g
val add_patterns_for_params_remove_local_defs : Environ.env -> Names.constructor -> 'a Glob_term.cases_pattern_g list -> 'a Glob_term.cases_pattern_g list
val empty_lvar : Ltac_pretype.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