diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-16 21:55:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-16 21:55:14 +0100 |
| commit | 7707396c5010d88c3d0be6ecee816d8da7ed0ee0 (patch) | |
| tree | 9229f1b9cf9102683bd3acb44b3131acb718d632 /toplevel | |
| parent | 29d7872c0159d2aab7264c0577a2f5a9dc7c90c9 (diff) | |
Fixing #5339 (anomaly with 'pat in record parameters).
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/record.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index b8dcf81fd..8d35e5a3d 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -108,7 +108,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = List.iter (function LocalRawDef (b, _) -> error default_binder_kind b | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalPattern _ -> assert false) ps + | LocalPattern (loc,_,_) -> + Loc.raise loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in let t', template = match t with |