package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Utilities about notation_constr
val eq_notation_constr : (Names.Id.t list * Names.Id.t list) -> Notation_term.notation_constr -> Notation_term.notation_constr -> bool
val strictly_finer_notation_constr : (Names.Id.t list * Names.Id.t list) -> Notation_term.notation_constr -> Notation_term.notation_constr -> bool

Tell if t1 is a strict refinement of t2 (this is a partial order and returning false does not mean that t2 is finer than t1)

Substitution of kernel names in interpretation data

Name of the special identifier used to encode recursive notations

val ldots_var : Names.Id.t
Translation back and forth between glob_constr and notation_constr

Translate a glob_constr into a notation given the list of variables bound by the notation; also interpret recursive patterns

Re-interpret a notation as a glob_constr, taking care of binders

type 'a binder_status_fun = {
  1. no : 'a -> 'a;
  2. restart_prod : 'a -> 'a;
  3. restart_lambda : 'a -> 'a;
  4. switch_prod : 'a -> 'a;
  5. switch_lambda : 'a -> 'a;
  6. slide : 'a -> 'a;
}
val glob_constr_of_notation_constr : ?loc:Loc.t -> Notation_term.notation_constr -> Glob_term.glob_constr
Matching a notation pattern against a glob_constr

match_notation_constr matches a glob_constr against a notation interpretation; raise No_match if the matching fails

exception No_match
val print_parentheses : bool ref
Matching a notation pattern against a glob_constr