diff options
| author | Emilio Jesus Gallego Arias | 2017-01-17 14:44:28 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 23:58:23 +0200 |
| commit | a9d151a31937724543d5269e72b0262c8764c46e (patch) | |
| tree | c88761514ebb3b4ff2691acf8dcfec6f13135d97 /vernac | |
| parent | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (diff) | |
[location] More located use.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 37ce231f96..95f5ad7cc2 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -112,7 +112,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = List.iter (function CLocalDef (b, _, _) -> error default_binder_kind b | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls - | CLocalPattern (loc,_,_) -> + | CLocalPattern (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 |