aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/notation.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index f2d113954b..f69d6f7d97 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1357,6 +1357,7 @@ let find_with_delimiters = function
match (String.Map.find scope !scope_map).delimiters with
| Some key -> Some (Some scope, Some key)
| None -> None
+ | exception Not_found -> None
let rec find_without_delimiters find (ntn_scope,ntn) = function
| OpenScopeItem scope :: scopes ->