Module Notation_term

type notation_constr =
| NRef of Names.GlobRef.t * Glob_term.glob_instance option
| NVar of Names.Id.t
| NApp of notation_constr * notation_constr list
| NProj of Names.Constant.t * Glob_term.glob_instance option * notation_constr list * notation_constr
| NHole of Glob_term.glob_evar_kind
| NGenarg of Genarg.glob_generic_argument
| NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
| NLambda of Names.Name.t * notation_constr option * notation_constr
| NProd of Names.Name.t * notation_constr option * notation_constr
| NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool
| NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr
| NCases of Constr.case_style * notation_constr option * (notation_constr * (Names.Name.t * (Names.inductive * Names.Name.t list) option)) list * (Glob_term.cases_pattern list * notation_constr) list
| NLetTuple of Names.Name.t list * Names.Name.t * notation_constr option * notation_constr * notation_constr
| NIf of notation_constr * Names.Name.t * notation_constr option * notation_constr * notation_constr
| NRec of Glob_term.glob_fix_kind * Names.Id.t array * (Names.Name.t * notation_constr option * notation_constr) list array * notation_constr array * notation_constr array
| NSort of Glob_term.glob_sort
| NCast of notation_constr * Constr.cast_kind option * notation_constr
| NInt of Uint63.t
| NFloat of Float64.t
| NArray of notation_constr array * notation_constr * notation_constr
type scope_name = string
type tmp_scope_name = scope_name
type subscopes = tmp_scope_name list * scope_name list
type extended_subscopes = Constrexpr.notation_entry_relative_level * subscopes
type notation_binder_kind =
| AsIdent
| AsName
| AsAnyPattern
| AsStrictPattern
type notation_binder_source =
| NtnBinderParsedAsConstr of notation_binder_kind
| NtnBinderParsedAsSomeBinderKind of notation_binder_kind
| NtnBinderParsedAsBinder
type notation_var_instance_type =
| NtnTypeConstr
| NtnTypeConstrList
| NtnTypeBinder of notation_binder_source
| NtnTypeBinderList of notation_binder_source
type notation_var_internalization_type =
| NtnInternTypeAny of scope_name option
| NtnInternTypeOnlyBinder

Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y

type notation_var_binders = Names.Id.Set.t

The set of other notation variables that are bound to a binder or binder list and that bind the given notation variable, for instance, in "{ x | P }" := (sigT (fun x => P), "x" is under an empty set of binders and "P" is under the binders bound to "x", that is, its notation_var_binders set is "x"

type interpretation = (Names.Id.t * (extended_subscopes * notation_var_binders * notation_var_instance_type)) list * notation_constr

This characterizes to what a notation is interpreted to

type reversibility_status =
| APrioriReversible
| HasLtac
| NonInjective of Names.Id.t list
type notation_interp_env = {
ninterp_var_type : notation_var_internalization_type Names.Id.Map.t;
ninterp_rec_vars : Names.Id.t Names.Id.Map.t;
}