diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-21 13:59:35 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-21 13:59:35 +0200 |
commit | bd81eaef87c5eb3a5d5bf398e151235e4e5c81a1 (patch) | |
tree | 72246effa2d991b2370aa77f7f8f00ce5fe6c395 /interp/topconstr.mli | |
parent | 9c352481f1a2d3a9c2e0e1f084d1c65521a0c438 (diff) |
Fix an error-prone error API.
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r-- | interp/topconstr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index ac98331c6..95d702f8d 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -46,4 +46,4 @@ val patntn_loc : (** For cases pattern parsing errors *) -val error_invalid_pattern_notation : ?loc:Loc.t -> 'a +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a |