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 /interp | |
| 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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |