diff options
| author | Hugo Herbelin | 2019-11-15 21:49:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:37:42 +0100 |
| commit | bf1e15181a2531a106fa643ca8e9233cb889af12 (patch) | |
| tree | 17de57d1f8d9efb537feaf2c201a0f17c85c29a8 /interp | |
| parent | 02cdbd221183b985460dedd49d74b07f4b647bcd (diff) | |
Fixes #4690: do not allow @f in notations when f is a notation variable.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f68f4e67b9..c39e61083d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c = (**********************************************************************) (* Syntax extensions *) +let check_not_notation_variable f ntnvars = + (* Check bug #4690 *) + match DAst.get f with + | GVar id when Id.Map.mem id ntnvars -> + user_err (str "Prefix @ is not applicable to notation variables.") + | _ -> + () + let option_mem_assoc id = function | Some (id',c) -> Id.equal id id' | None -> false @@ -2063,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref in + check_not_notation_variable f ntnvars; (* Rem: GApp(_,f,[]) stands for @f *) if args = [] then DAst.make ?loc @@ GApp (f,[]) else smart_gapp f loc (intern_args env args_scopes (List.map fst args)) |