diff options
| author | Emilio Jesus Gallego Arias | 2018-06-03 00:35:56 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-03 00:35:56 +0200 |
| commit | 5c93d722426a552f4cf1ce93bcd3dbaf14948b6f (patch) | |
| tree | 6d5b00f3afdf78ca1a01007c2b66c0becb5f483f /interp/constrintern.ml | |
| parent | fb406f8b33014c63139bbafd472b6afe7a4f72c9 (diff) | |
| parent | fd33e3875b872f8b83c350427a9809e68d7fe009 (diff) | |
Merge PR #7681: Fixes #7636: location missing on deprecated compatibility notations.
Diffstat (limited to 'interp/constrintern.ml')
| -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 45c0e9c42d..1691ff6d86 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -999,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args = match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in |