package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val map_glob_sort_gen : ('a -> 'b) -> 'a Glob_term.glob_sort_gen -> 'b Glob_term.glob_sort_gen

Equalities

val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a Glob_term.glob_sort_gen -> 'a Glob_term.glob_sort_gen -> bool
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

Expect a Prop/SProp/Set/Type universe; raise ComplexSort if contains a max, an increment, or a flexible universe

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_kind_eq : Constr.cast_kind -> Constr.cast_kind -> bool
val glob_constr_eq : 'a Glob_term.glob_constr_g -> 'a Glob_term.glob_constr_g -> bool

Operations on glob_constr

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

Apply a list of arguments to a glob_constr

val binding_kind_eq : Glob_term.binding_kind -> Glob_term.binding_kind -> bool

Equality on binding_kind

Ensure traversal from left to right

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

map_pattern_binders f m c applies f to all the binding names in a pattern-matching expression (Glob_term.glob_constr_r.GCases) represented here by its relevant components m and c. It is used to interpret Ltac-bound names both in pretyping and printing of terms.

map_pattern f m c applies f to the return predicate and the right-hand side of a pattern-matching expression (Glob_term.glob_constr_r.GCases) represented here by its relevant components m and c.

val cases_pattern_of_glob_constr : Environ.env -> Names.Name.t -> 'a Glob_term.glob_constr_g -> 'a Glob_term.cases_pattern_g

Conversion from glob_constr to cases pattern, if possible

Evaluation is forced. Take the current alias as parameter,

  • raises Not_found

    if translation is impossible

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

A canonical encoding of cases pattern into constr such that composed with cases_pattern_of_glob_constr Anonymous gives identity

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