package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val sort_name_expr_eq : Constrexpr.sort_name_expr -> Constrexpr.sort_name_expr -> bool
val univ_level_expr_eq : Constrexpr.univ_level_expr -> Constrexpr.univ_level_expr -> bool
val sort_expr_eq : Constrexpr.sort_expr -> Constrexpr.sort_expr -> bool
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
val constr_expr_eq : Constrexpr.constr_expr -> Constrexpr.constr_expr -> 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