diff options
| author | herbelin | 2009-10-28 17:45:48 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-28 17:45:48 +0000 |
| commit | d491c4974ad7ec82a5369049c27250dd07de852c (patch) | |
| tree | e00857f10948fcf48f5688b96a3a24fb7d67700c | |
| parent | d5b03d4b052023012b859071e2bd6ff754256cab (diff) | |
Made that notations to names behave like the names they refer to wrt
implicit arguments and scope (use Implicit Arguments or Arguments
Scope commands instead if not the desired behaviour).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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). |