diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-12-02 14:28:29 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-12-02 14:55:54 +0100 |
| commit | 16504ad480a920e1800d52f5adbea8ddecefbeb0 (patch) | |
| tree | 7ce520895f73c0d906ee5f03d245d1f445fdf2f2 /interp | |
| parent | 315aac9ae0d411c10849c421d5dfd8e134919233 (diff) | |
Fix a bug in externalisation which prevented printing of projections
using dot notation.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5160f07af..ba20f9fa0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -447,8 +447,8 @@ let is_projection nargs = function | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then None - else Some n + if n <= nargs then Some n + else None with Not_found -> None) | _ -> None |