diff options
| author | herbelin | 2003-09-18 18:41:39 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-18 18:41:39 +0000 |
| commit | 184550121303fe264150996f74d64dc7a149099f (patch) | |
| tree | a4e789402a6a6d2ee7c80c1f4b8b8916247e7a41 | |
| parent | 4abc3dab7b2e143544be1f1c963001dd0b9af4d5 (diff) | |
Parsing correct des explicites en cas de projection
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4411 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b4edaaf1ec..c07522cc70 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -524,6 +524,11 @@ let internalise sigma env allow_soapp lvar c = check_projection isproj (List.length args) f; RApp (loc, f, intern_args env args_scopes args) | CApp (loc, (isproj,f), args) -> + let isproj,f,args = match f with + (* Compact notations like "t.(f args') args" *) + | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args + (* Don't compact "(f args') args" to resolve implicits separately *) + | _ -> isproj,f,args in let (c, impargs, args_scopes) = match f with | CRef ref -> intern_reference env lvar ref @@ -532,6 +537,7 @@ let internalise sigma env allow_soapp lvar c = let args = intern_impargs c env impargs args_scopes args in check_projection isproj (List.length args) c; (match c with + (* Now compact "(f args') args" *) | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) | CCases (loc, (po,rtnpo), tms, eqns) -> |