diff options
| author | Matthieu Sozeau | 2014-08-08 15:33:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-08 15:33:06 +0200 |
| commit | ff884c172697c1452db535cdbd6babceb556c428 (patch) | |
| tree | ac7092faa6368ff85eacc68385c67b118b0280d4 /interp/constrextern.ml | |
| parent | 758f031bc2e2d4a5ece6d515533fafe3e9df98d5 (diff) | |
Change internalization of primitive projections to allow parsing [p t] as
a primitive application only if all parameters of [p] are implicit, falling
back to the internalization of the eta-expanded version otherwise. This makes
apply [p] succeed even if its record argument is not implicit, ensuring better
compatibility.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9c2f8bcd3f..759410042f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -479,13 +479,13 @@ let explicitize loc inctx impl (cf,primproj,f) args = | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) | [], _ -> [] in match is_projection primproj (List.length args) cf with - | Some i -> + | Some i as ip -> if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then let args = exprec 1 (args,impl) in if primproj then CApp (loc, (None, f), args) - else + else let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in - CAppExpl (loc,(Some i,f',us), List.map fst args) + CAppExpl (loc,(ip,f',us),List.map fst args) else let (args1,args2) = List.chop i args in let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in @@ -497,8 +497,7 @@ let explicitize loc inctx impl (cf,primproj,f) args = match cf with | Some (ConstRef p) when not primproj && Environ.is_projection p (Global.env ()) -> (* Eta-expanded version of projection *) - let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in - CAppExpl (loc, (None, f', us), List.map fst args) + CApp (loc, (None, f), args) | _ -> if List.is_empty args then f else CApp (loc, (None, f), args) let extern_global loc impl f us = |