package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val asymmetric_patterns : bool Pervasives.ref
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 ids_of_cases_indtype : Constrexpr.cases_pattern_expr -> Names.Id.Set.t
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 ntn_loc : ?loc:Loc.t -> Constrexpr.constr_notation_substitution -> string -> (int * int) list
val patntn_loc : ?loc:Loc.t -> Constrexpr.cases_pattern_notation_substitution -> string -> (int * int) list
val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
OCaml

Innovation. Community. Security.