diff options
Diffstat (limited to 'debugger/pattern_matching.ml')
| -rw-r--r-- | debugger/pattern_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debugger/pattern_matching.ml b/debugger/pattern_matching.ml index 26e5a61f4..a04dcae5b 100644 --- a/debugger/pattern_matching.ml +++ b/debugger/pattern_matching.ml @@ -60,7 +60,7 @@ let error_matching () = let same_name {qualid = name1} = function GRname name2 -> - (name2 = "") or (name1.id = name2) + (name2 = "") || (name1.id = name2) | GRmodname name2 -> name1 = name2 |