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 | |
| parent | 02cdbd221183b985460dedd49d74b07f4b647bcd (diff) | |
Fixes #4690: do not allow @f in notations when f is a notation variable.
| -rw-r--r-- | interp/constrintern.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/bug_4690.v | 3 |
2 files changed, 12 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)) diff --git a/test-suite/bugs/bug_4690.v b/test-suite/bugs/bug_4690.v new file mode 100644 index 0000000000..f50866a990 --- /dev/null +++ b/test-suite/bugs/bug_4690.v @@ -0,0 +1,3 @@ +(* Check that @f is not allowed in notation when f is a notation variable *) + +Fail Notation "# g" := (@g O) (at level 0). |