Revert specific syntax for primitive projections, avoiding ugly

contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.

1 files changed, 4 insertions, 59 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 66f51b19e6..56780e2402 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1312,7 +1312,6 @@ let get_implicit_name n imps =
 
 let set_hole_implicit i b = function
   | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None)
-  | GProj (loc,p,_) -> (loc,Evar_kinds.ImplicitArg (ConstRef p,i,b),None)
   | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
@@ -1463,14 +1462,8 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
 	    lvar us args ref 
 	in
-	  (match isproj, isprojf with
-	  | Some i, Some (r, n) -> (* Explicit application of primitive projection *)
-	    let scopes = proj_scopes n args_scopes in
-	    let args = intern_args env scopes (List.map fst args) in
-	      GApp (loc, GProj (loc, r, List.hd args), List.tl args)
-	  | _ ->
-	    (* Rem: GApp(_,f,[]) stands for @f *)
-	    GApp (loc, f, intern_args env args_scopes (List.map fst args)))
+	  (* Rem: GApp(_,f,[]) stands for @f *)
+	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
 
     | CApp (loc, (isproj,f), args) ->
         let isproj,f,args = match f with
@@ -1726,58 +1719,10 @@ 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 =
-    match l with
-    | hd :: tl -> None :: tl
-    | [] -> []
-
-  and projection_application_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_application_implicits (pred n) noargs tl
-      else None
-    | _ -> None
-
   and apply_impargs (isproj,isprojf) c env imp subscopes l loc = 
     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) -> (* A primitive projection *)
-	let subscopes = proj_scopes n subscopes in
-	if isproj != None then (* In projection notation: we remove the parameters *)
-	  let imp = projection_implicits (Global.env()) r imp in
-	  let imp = make_first_explicit imp in (* For the record argument *)
-	  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
-	    | _ -> assert false)
-	else (* Not in projection notation, parse as primitive only if the implicits
-		allow *)
-	  (match projection_application_implicits n (List.is_empty l) imp with
-	  | Some imp ->
-	    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 ()
+    let l = intern_impargs c env imp subscopes l in
+      smart_gapp c loc l
 
   and smart_gapp f loc = function
     | [] -> f