package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
val constr_expr_eq : Constrexpr.constr_expr -> Constrexpr.constr_expr -> bool
val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
val binder_kind_eq : Constrexpr.binder_kind -> Constrexpr.binder_kind -> bool
val constr_loc : Constrexpr.constr_expr -> Loc.t option
val cases_pattern_expr_loc : Constrexpr.cases_pattern_expr -> Loc.t option
val local_binders_loc : Constrexpr.local_binder_expr list -> Loc.t option
val coerce_reference_to_id : Libnames.qualid -> Names.Id.t
val coerce_to_id : Constrexpr.constr_expr -> Names.lident
val coerce_to_name : Constrexpr.constr_expr -> Names.lname
val coerce_to_cases_pattern_expr : Constrexpr.constr_expr -> Constrexpr.cases_pattern_expr
val default_binder_kind : Constrexpr.binder_kind
val names_of_local_binders : Constrexpr.local_binder_expr list -> Names.lname list
val names_of_local_assums : Constrexpr.local_binder_expr list -> Names.lname list
val fold_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> 'b -> Constrexpr.constr_expr -> 'b) -> 'a -> 'b -> Constrexpr.constr_expr -> 'b
val map_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> Constrexpr.constr_expr -> Constrexpr.constr_expr) -> 'a -> Constrexpr.constr_expr -> Constrexpr.constr_expr
val free_vars_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t
val occur_var_constr_expr : Names.Id.t -> Constrexpr.constr_expr -> bool
val names_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t
val ntn_loc : ?loc:Loc.t -> Constrexpr.constr_notation_substitution -> Constrexpr.notation -> (int * int) list
val patntn_loc : ?loc:Loc.t -> Constrexpr.cases_pattern_notation_substitution -> Constrexpr.notation -> (int * int) list
val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
val asymmetric_patterns : bool ref
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