aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.mli
diff options
context:
space:
mode:
authorEnrico Tassi2015-03-30 11:30:53 +0200
committerEnrico Tassi2015-03-30 11:30:53 +0200
commitaeec29a177e8f1c89996c0449e4cd81ca3ca4377 (patch)
treecc39f942a75fd621633b1ac0999bbe4b3918fcfd /interp/notation.mli
parent224d3b0e8be9b6af8194389141c9508504cf887c (diff)
parent41e4725805588b3fffdfdc0cd5ee6859de1612b5 (diff)
Merge branch 'v8.5' into trunk
Diffstat (limited to 'interp/notation.mli')
-rw-r--r--interp/notation.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/interp/notation.mli b/interp/notation.mli
index c66115cbdd..854c52b2c7 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -140,6 +140,10 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
notation -> delimiters option -> global_reference
+(** Checks for already existing notations *)
+val exists_notation_in_scope : scope_name option -> notation ->
+ interpretation -> bool
+
(** Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope :
bool (** true=local *) -> global_reference -> scope_name option list -> unit