diff options
| author | Pierre Roux | 2021-01-02 12:44:23 +0100 |
|---|---|---|
| committer | Pierre Roux | 2021-01-18 12:09:11 +0100 |
| commit | 1b0f76026a553bcd76efb2bf99048235ad847ada (patch) | |
| tree | b6da940105a0962fd5f3226e620a97a627eefe99 | |
| parent | 039f04c2caf7c8da380ca8d582e9edae3e6d5c06 (diff) | |
Print primitive constants in debuger
This was raising a Not_found exception due to the unknown scope.
| -rw-r--r-- | interp/notation.ml | 1 |
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 -> |