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.

2 files changed, 43 insertions, 31 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9c2f8bcd3..759410042 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 =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6ae5ca352..8f76bbb61 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1675,7 +1675,6 @@ let internalize globalenv env allow_patvar lvar c =
     it_mkGLambda loc2 bl (intern env body)
 
   and intern_impargs c env l subscopes args =
-    let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
     if !parsing_explicit then
       if Id.Map.is_empty eargs then intern_args env subscopes rargs
@@ -1713,35 +1712,49 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern_args env subscopes rargs
     in aux 1 l subscopes eargs rargs
 
-  and make_first_explicit (l, r) =
-    match r with
-    | hd :: tl -> l, None :: tl
-    | [] -> l, []
+  and make_first_explicit l =
+    match l with
+    | hd :: tl -> None :: tl
+    | [] -> []
+
+  and projection_implicits n noargs l = 
+    if n == 0 then Some l
+    else match l with 
+    | hd :: tl when is_status_implicit hd ->
+      if maximal_insertion_of hd || not noargs then
+	projection_implicits (pred n) noargs tl
+      else None
+    | _ -> None
 
   and apply_impargs (isproj,isprojf) c env imp subscopes l loc = 
-    match isprojf with
-    | Some (r, n) ->
-      let imp, subscopes = proj_impls r imp, proj_scopes n subscopes in
-      let imp = 
-	if isproj != None then
-	  (* Drop first implicit which corresponds to record given in c.(p) notation *)
-	  List.map make_first_explicit imp 
-	else imp
-      in
-      let l = intern_impargs c env imp subscopes l in
-	(match c, l with
-	| GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest ->
-	  let proj = GProj (Loc.merge loc'' (loc_of_glob_constr hd), f, hd) in
-	    if List.is_empty tl then smart_gapp proj loc rest
-	    else GApp (loc, proj, tl @ rest)
-	| GRef (loc', ConstRef f, _), hd :: tl -> 
-	  let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in
-	    smart_gapp proj loc tl
-	| _ -> user_err_loc (loc, "apply_impargs", 
-			     str"Projection is not applied to enough arguments"))
-    | None ->
+    let imp = select_impargs_size (List.length l) imp in
+    let default () =
       let l = intern_impargs c env imp subscopes l in
 	smart_gapp c loc l
+    in
+      match isprojf with
+      | Some (r, n) ->
+	(match projection_implicits n (List.is_empty l) imp with
+	| Some imp -> 
+	  let subscopes = proj_scopes n subscopes in
+	  let imp = 
+	    if isproj != None then
+	      (* Drop first implicit which corresponds to record given in c.(p) notation *)
+	      make_first_explicit imp
+	    else imp
+	  in
+	  let l = intern_impargs c env imp subscopes l in
+	    (match c, l with
+	    | GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest ->
+	      let proj = GProj (Loc.merge loc'' (loc_of_glob_constr hd), f, hd) in
+		if List.is_empty tl then smart_gapp proj loc rest
+		else GApp (loc, proj, tl @ rest)
+	    | GRef (loc', ConstRef f, _), hd :: tl -> 
+	      let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in
+		smart_gapp proj loc tl
+	    | _ -> default ())
+	| None -> default ())
+      | None -> default ()
 
   and smart_gapp f loc = function
     | [] -> f