Module Ltac2_plugin.Tac2syn

module Tac2Scope : module type of Names.KerName

Common APIs on name tables.

val declare_scope : Names.Id.t -> unit
val open_scope : Libobject.locality -> Libnames.qualid -> unit
val close_scope : Libobject.locality -> Libnames.qualid -> unit
val default_scope : unit -> Tac2Scope.t
val current_scopes : unit -> Tac2Scope.t list
module Tac2Custom : module type of Names.KerName

Common APIs on name tables.

val find_custom_entry : Tac2Custom.t -> Tac2expr.raw_tacexpr Procq.Entry.t

NB: Do not save the result of this function across summary resets, the Entry.t gets regenerated on (parsing) summary unfreeze.

module Syntax : sig ... end
type syntax_class_rule =
| SyntaxRule : 'a Syntax.t * ('a -> Tac2expr.raw_tacexpr) -> syntax_class_rule
type used_levels
val no_used_levels : used_levels
val union_used_levels : used_levels -> used_levels -> used_levels
type 'glb syntax_class_decl = {
intern_synclass : Tac2expr.sexpr list -> used_levels * 'glb;
interp_synclass : 'glb -> syntax_class_rule;
}
val register_syntax_class : Names.Id.t -> _ syntax_class_decl -> unit

Create a new syntax class with the provided name

type syntax_class
val intern_syntax_class : Tac2expr.sexpr -> used_levels * syntax_class

Use this to internalize the syntax class arguments for interpretation functions

val interp_syntax_class : syntax_class -> syntax_class_rule

Use this to interpret the syntax class arguments for interpretation functions

type notation_data =
| UntypedNota of Tac2expr.raw_tacexpr
| TypedNota of {
nota_prms : int;
nota_argtys : int Tac2expr.glb_typexpr Names.Id.Map.t;
nota_ty : int Tac2expr.glb_typexpr;
nota_body : Tac2expr.glb_tacexpr;
}
val interp_notation : ?loc:Loc.t -> Tac2Scope.t list -> Tac2expr.tacsyn -> notation_data * (Names.lname * Tac2expr.raw_tacexpr) list
type ('scope, 'body) notation_interpretation
val ltac2_notation_cat : Libobject.category
type notation_target = {
target_entry : Libnames.qualid option;
target_level : int option;
target_scope : Libnames.qualid option;
}
val pr_register_notation : Tac2expr.sexpr list -> notation_target -> Tac2expr.raw_tacexpr -> Pp.t
val register_notation : Attributes.vernac_flags -> Tac2expr.sexpr list -> notation_target -> 'body -> (Libnames.qualid option, 'body) notation_interpretation

Does not handle the deprecated abbreviation syntax

val intern_notation_interpretation : (Names.Id.Set.t -> 'raw -> 'glb) -> (Libnames.qualid option, 'raw) notation_interpretation -> (Tac2Scope.t, 'glb) notation_interpretation
val register_notation_interpretation : (Tac2Scope.t, notation_data) notation_interpretation -> unit
val register_custom_entry : Names.lident -> unit
module Internal : sig ... end