diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | interp/constrintern.ml | 5 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
3 files changed, 15 insertions, 1 deletions
@@ -46,6 +46,11 @@ Tactic Language - Support for parsing non-empty lists with separators in tactic notations. +Language + +- Notations to names now behave like the names they refer to wrt implicit + arguments and interpretation scopes. + Vernacular commands - New command "Timeout <n> <command>." interprets a command and a timeout diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8b60cff50d..299f742d1a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -358,7 +358,9 @@ let intern_qualid loc qid intern env args = RRef (loc, ref), args | SynDef sp -> Dumpglob.add_glob_kn loc sp; - let (ids,c) = Syntax_def.search_syntactic_definition loc sp in + match Syntax_def.search_syntactic_definition loc sp with + | [],ARef ref -> RRef (loc, ref), args + | (ids,c) -> 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 @@ -949,6 +951,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let args = List.map (fun a -> (a,None)) args in intern_applied_reference intern env lvar args ref in check_projection isproj (List.length args) f; + if args = [] then f else RApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 7d7bcc71ec..316bede93b 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -48,3 +48,9 @@ Definition foo P := let '(exists x, Q) := P in x = Q :> nat. Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat (at level 200, x ident, right associativity, y at level 69). + +(* Check that notations to atomic references preserve implicit arguments *) + +Notation eq := @eq. + +Check (eq 0 0). |