diff options
| author | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
| commit | 99cdbc25a3a92545544a087ed55240c488b42fc9 (patch) | |
| tree | 4b9f80d7ae15a421b5745dec138759a37cf68da6 /interp | |
| parent | 1c620d266885086e076011917d5b1d28af299ea1 (diff) | |
Fix bug #3289
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 475f8d396c..841a895849 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1496,7 +1496,7 @@ let internalize globalenv env allow_patvar lvar c = let cargs = sort_fields true loc fs (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), None) :: l) - in + in begin match cargs with | None -> user_err_loc (loc, "intern", str"No constructor inference.") |