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.

7 files changed, 123 insertions, 152 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1ff1b903f..823f5ef64 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -31,6 +31,8 @@ let dl = Loc.ghost
 (** Should we keep details of universes during detyping ? *)
 let print_universes = Flags.univ_print
 
+let add_name na b t (nenv, env) = add_name na nenv, push_rel (na, b, t) env
+
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
@@ -215,7 +217,7 @@ let lookup_index_as_renamed env t n =
 (**********************************************************************)
 (* Fragile algorithm to reverse pattern-matching compilation          *)
 
-let update_name na ((_,e),c) =
+let update_name na ((_,(e,_)),c) =
   match na with
   | Name _ when force_wildcard () && noccurn (List.index Name.equal na e) c ->
       Anonymous
@@ -223,19 +225,20 @@ let update_name na ((_,e),c) =
       na
 
 let rec decomp_branch ndecls nargs nal b (avoid,env as e) c =
-  let flag = if b then RenamingForGoal else RenamingForCasesPattern (env,c) in
+  let flag = if b then RenamingForGoal else RenamingForCasesPattern (fst env,c) in
   if Int.equal ndecls 0 then (List.rev nal,(e,c))
   else
-    let na,c,f,nargs' =
+    let na,c,f,nargs',body,t =
       match kind_of_term (strip_outer_cast c) with
-	| Lambda (na,_,c) -> na,c,compute_displayed_let_name_in,nargs-1
-	| LetIn (na,_,_,c) when ndecls>nargs ->
-            na,c,compute_displayed_name_in,nargs
-	| _ ->
+	| Lambda (na,t,c) -> na,c,compute_displayed_let_name_in,nargs-1,None,t
+	| LetIn (na,b,t,c) when ndecls>nargs ->
+            na,c,compute_displayed_name_in,nargs,Some b,t
+	| LetIn (na,b,t,c) ->
 	    Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])),
-	    compute_displayed_name_in,nargs-1 in
+	    compute_displayed_name_in,nargs-1,Some b,t 
+	| _ -> assert false in
     let na',avoid' = f flag avoid na c in
-    decomp_branch (ndecls-1) nargs' (na'::nal) b (avoid',add_name na' env) c
+    decomp_branch (ndecls-1) nargs' (na'::nal) b (avoid',add_name na' body t env) c
 
 let rec build_tree na isgoal e ci cl =
   let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
@@ -250,7 +253,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
   | na::nal ->
     match kind_of_term c with
     | Case (ci,p,c,cl) when
-        eq_constr c (mkRel (List.index Name.equal na (snd e)))
+        eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
 	&& (* don't contract if p dependent *)
 	computable p (ci.ci_pp_info.ind_nargs) ->
 	let clauses = build_tree na isgoal e ci cl in
@@ -393,10 +396,10 @@ let detype_instance l =
   if Univ.Instance.is_empty l then None
   else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l)))
 
-let rec detype isgoal avoid env sigma t =
+let rec detype flags avoid env sigma t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
-      (try match lookup_name_of_rel n env with
+      (try match lookup_name_of_rel n (fst env) with
 	 | Name id   -> GVar (dl, id)
 	 | Anonymous -> !detype_anonymous dl n
        with Not_found ->
@@ -411,19 +414,19 @@ let rec detype isgoal avoid env sigma t =
 	 with Not_found -> GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
-        detype isgoal avoid env sigma c1
+        detype flags avoid env sigma c1
     | Cast (c1,k,c2) ->
-        let d1 = detype isgoal avoid env sigma c1 in
-	let d2 = detype isgoal avoid env sigma c2 in
+        let d1 = detype flags avoid env sigma c1 in
+	let d2 = detype flags avoid env sigma c2 in
     let cast = match k with
     | VMcast -> CastVM d2
     | NATIVEcast -> CastNative d2
     | _ -> CastConv d2
     in
 	GCast(dl,d1,cast)
-    | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env sigma na ty c
-    | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env sigma na ty c
-    | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env sigma na b c
+    | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c
+    | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c
+    | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c
     | App (f,args) ->
       let mkapp f' args' = 
  	match f' with
@@ -431,66 +434,79 @@ let rec detype isgoal avoid env sigma t =
  	  GApp (dl,f',args''@args')
  	| _ -> GApp (dl,f',args')
       in
-	mkapp (detype isgoal avoid env sigma f)
-	  (Array.map_to_list (detype isgoal avoid env sigma) args)
+	mkapp (detype flags avoid env sigma f)
+	  (Array.map_to_list (detype flags avoid env sigma) args)
     | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
     | Proj (p,c) ->
-        GProj (dl, p, detype isgoal avoid env sigma c)
+      (try 
+	 let ty = Retyping.get_type_of (snd env) sigma c in
+	 let (ind, args) = Inductive.find_rectype (snd env) ty in
+	   GApp (dl, GRef (dl, ConstRef p, None), 
+		 List.map (detype flags avoid env sigma) (args @ [c]))
+       with e when fst flags (* lax mode, used by debug printers only *) ->
+	 GApp (dl, GRef (dl, ConstRef p, None), 
+	       [detype flags avoid env sigma c])
+       | e -> raise e)
     | Evar (evk,cl) ->
       let id,l =
         try Evd.evar_ident evk sigma,
-            Evd.evar_instance_array (fun id c -> try let n = List.index Name.equal (Name id) env in isRelN n c with Not_found -> isVarId id c) (Evd.find sigma evk) cl
+          Evd.evar_instance_array 
+	    (fun id c -> 
+	      try let n = List.index Name.equal (Name id) (fst env) in 
+		    isRelN n c 
+	      with Not_found -> isVarId id c) 
+	    (Evd.find sigma evk) cl
         with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), [] in
         GEvar (dl,id,
-               List.map (on_snd (detype isgoal avoid env sigma)) l)
+               List.map (on_snd (detype flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
 	GRef (dl, IndRef ind_sp, detype_instance u)
     | Construct (cstr_sp,u) ->
 	GRef (dl, ConstructRef cstr_sp, detype_instance u)
     | Case (ci,p,c,bl) ->
 	let comp = computable p (ci.ci_pp_info.ind_nargs) in
-	detype_case comp (detype isgoal avoid env sigma)
-	  (detype_eqns isgoal avoid env sigma ci comp)
+	detype_case comp (detype flags avoid env sigma)
+	  (detype_eqns flags avoid env sigma ci comp)
 	  is_nondep_branch avoid
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs)
 	  (Some p) c bl
-    | Fix (nvn,recdef) -> detype_fix isgoal avoid env sigma nvn recdef
-    | CoFix (n,recdef) -> detype_cofix isgoal avoid env sigma n recdef
+    | Fix (nvn,recdef) -> detype_fix flags avoid env sigma nvn recdef
+    | CoFix (n,recdef) -> detype_cofix flags avoid env sigma n recdef
 
-and detype_fix isgoal avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
   let def_avoid, def_env, lfi =
-    Array.fold_left
-      (fun (avoid, env, l) na ->
+    Array.fold_left2
+      (fun (avoid, env, l) na ty ->
 	 let id = next_name_away na avoid in
-	 (id::avoid, add_name (Name id) env, id::l))
-      (avoid, env, []) names in
+	 (id::avoid, add_name (Name id) None ty env, id::l))
+      (avoid, env, []) names tys in
   let n = Array.length tys in
   let v = Array.map3
-    (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env sigma c (lift n t))
+    (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t))
     bodies tys vn in
   GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-and detype_cofix isgoal avoid env sigma n (names,tys,bodies) =
+and detype_cofix flags avoid env sigma n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
-    Array.fold_left
-      (fun (avoid, env, l) na ->
+    Array.fold_left2
+      (fun (avoid, env, l) na ty ->
 	 let id = next_name_away na avoid in
-	 (id::avoid, add_name (Name id) env, id::l))
-      (avoid, env, []) names in
+	 (id::avoid, add_name (Name id) None ty env, id::l))
+      (avoid, env, []) names tys in
   let ntys = Array.length tys in
   let v = Array.map2
-    (fun c t -> share_names isgoal 0 [] def_avoid def_env sigma c (lift ntys t))
+    (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t))
     bodies tys in
   GRec(dl,GCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-and share_names isgoal n l avoid env sigma c t =
+and share_names flags n l avoid env sigma c t =
   match kind_of_term c, kind_of_term t with
     (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
@@ -498,67 +514,67 @@ and share_names isgoal n l avoid env sigma c t =
             Name _, _ -> na
           | _, Name _ -> na'
           | _ -> na in
-        let t = detype isgoal avoid env sigma t in
+        let t' = detype flags avoid env sigma t in
 	let id = next_name_away na avoid in
-        let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env sigma c c'
+        let avoid = id::avoid and env = add_name (Name id) None t env in
+        share_names flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
-        let t' = detype isgoal avoid env sigma t' in
-        let b = detype isgoal avoid env sigma b in
+        let t'' = detype flags avoid env sigma t' in
+        let b' = detype flags avoid env sigma b in
 	let id = next_name_away na avoid in
-        let avoid = id::avoid and env = add_name (Name id) env in
-        share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env sigma c (lift 1 t)
+        let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in
+        share_names flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
-	share_names isgoal n l avoid env sigma c (subst1 b t)
+	share_names flags n l avoid env sigma c (subst1 b t)
     (* If it is an open proof: we cheat and eta-expand *)
     | _, Prod (na',t',c') when n > 0 ->
-        let t' = detype isgoal avoid env sigma t' in
+        let t'' = detype flags avoid env sigma t' in
 	let id = next_name_away na' avoid in
-        let avoid = id::avoid and env = add_name (Name id) env in
+        let avoid = id::avoid and env = add_name (Name id) None t' env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma appc c'
+        share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
-        let c = detype isgoal avoid env sigma c in
-        let t = detype isgoal avoid env sigma t in
+        let c = detype flags avoid env sigma c in
+        let t = detype flags avoid env sigma t in
         (List.rev l,c,t)
 
-and detype_eqns isgoal avoid env sigma ci computable constructs consnargsl bl =
+and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
-    let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
-    List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env sigma c))
+    let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in
+    List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
       mat
   with e when Errors.noncritical e ->
     Array.to_list
-      (Array.map3 (detype_eqn isgoal avoid env sigma) constructs consnargsl bl)
+      (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl)
 
-and detype_eqn isgoal avoid env sigma constr construct_nargs branch =
-  let make_pat x avoid env b ids =
+and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
+  let make_pat x avoid env b body ty ids =
     if force_wildcard () && noccurn 1 b then
-      PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
+      PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids
     else
-      let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (env,b) in
+      let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
       let na,avoid' = compute_displayed_name_in flag avoid x b in
-      PatVar (dl,na),avoid',(add_name na env),add_vname ids na
+      PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na
   in
   let rec buildrec ids patlist avoid env n b =
     if Int.equal n 0 then
       (dl, Id.Set.elements ids,
        [PatCstr(dl, constr, List.rev patlist,Anonymous)],
-       detype isgoal avoid env sigma b)
+       detype flags avoid env sigma b)
     else
       match kind_of_term b with
-	| Lambda (x,_,b) ->
-	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
+	| Lambda (x,t,b) ->
+	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in
             buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
 
-	| LetIn (x,_,_,b) ->
-	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
-            buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
+	| LetIn (x,b,t,b') ->
+	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b' (Some b) t ids in
+            buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b'
 
 	| Cast (c,_,_) ->    (* Oui, il y a parfois des cast *)
 	    buildrec ids patlist avoid env n c
@@ -568,24 +584,24 @@ and detype_eqn isgoal avoid env sigma constr construct_nargs branch =
             (* nommage de la nouvelle variable *)
 	    let new_b = applist (lift 1 b, [mkRel 1]) in
             let pat,new_avoid,new_env,new_ids =
-	      make_pat Anonymous avoid env new_b ids in
+	      make_pat Anonymous avoid env new_b None mkProp ids in
 	    buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
 
   in
   buildrec Id.Set.empty [] avoid env construct_nargs branch
 
-and detype_binder isgoal bk avoid env sigma na ty c =
-  let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
+and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
+  let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
   let na',avoid' = match bk with
   | BLetIn -> compute_displayed_let_name_in flag avoid na c
   | _ -> compute_displayed_name_in flag avoid na c in
-  let r =  detype isgoal avoid' (add_name na' env) sigma c in
+  let r =  detype flags avoid' (add_name na' body ty env) sigma c in
   match bk with
-  | BProd -> GProd (dl, na',Explicit,detype false avoid env sigma ty, r)
-  | BLambda -> GLambda (dl, na',Explicit,detype false avoid env sigma ty, r)
-  | BLetIn -> GLetIn (dl, na',detype false avoid env sigma ty, r)
+  | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
+  | BLambda -> GLambda (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
+  | BLetIn -> GLetIn (dl, na',detype (lax,false) avoid env sigma (Option.get body), r)
 
-let detype_rel_context where avoid env sigma sign =
+let detype_rel_context ?(lax=false) where avoid env sigma sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
@@ -596,15 +612,20 @@ let detype_rel_context where avoid env sigma sign =
 	| Some c ->
 	    if b != None then
 	      compute_displayed_let_name_in
-                (RenamingElsewhereFor (env,c)) avoid na c
+                (RenamingElsewhereFor (fst env,c)) avoid na c
 	    else
 	      compute_displayed_name_in
-                (RenamingElsewhereFor (env,c)) avoid na c in
-      let b = Option.map (detype false avoid env sigma) b in
-      let t = detype false avoid env sigma t in
-      (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
+                (RenamingElsewhereFor (fst env,c)) avoid na c in
+      let b' = Option.map (detype (lax,false) avoid env sigma) b in
+      let t' = detype (lax,false) avoid env sigma t in
+      (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest
   in aux avoid env (List.rev sign)
 
+let detype_names isgoal avoid nenv env sigma t = 
+  detype (false,isgoal) avoid (nenv,env) sigma t
+let detype ?(lax=false) isgoal avoid env sigma t =
+  detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
+
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)
 
@@ -624,7 +645,7 @@ let rec subst_glob_constr subst raw =
   | GRef (loc,ref,u) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         detype false [] [] Evd.empty t
+         detype false [] (Global.env()) Evd.empty t
 
   | GVar _ -> raw
   | GEvar _ -> raw
@@ -636,12 +657,6 @@ let rec subst_glob_constr subst raw =
 	if r' == r && rl' == rl then raw else
 	  GApp(loc,r',rl')
 
-  | GProj (loc,p,c) -> 
-    let p' = subst_constant subst p in
-    let c' = subst_glob_constr subst c in
-      if p' == p && c' == c then raw
-      else GProj (loc,p',c')
-
   | GLambda (loc,n,bk,r1,r2) ->
       let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 8a8302b8b..b2fc92557 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -28,8 +28,9 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
    [ctx] gives the names of the free variables *)
 
-val detype : bool -> Id.t list -> names_context ->
-  evar_map -> constr -> glob_constr
+val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr
+
+val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr
 
 val detype_case :
   bool -> ('a -> glob_constr) ->
@@ -41,7 +42,7 @@ val detype_case :
 
 val detype_sort : sorts -> glob_sort
 
-val detype_rel_context : constr option -> Id.t list -> names_context ->
+val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
   evar_map -> rel_context -> glob_decl list
 
 (** look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 47955e8e0..0fd508604 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -456,7 +456,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
-	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in
+	     pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) 
+		 ++ fnl ()) in
   match (flex_kind_of_term ts env term1 sk1, flex_kind_of_term ts env term2 sk2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cfbff80a9..f02d7623d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -21,6 +21,8 @@ open Evd
 open Reductionops
 open Pretype_errors
 
+(** Combinators *)
+
 let evd_comb0 f evdref =
   let (evd',x) = f !evdref in
     evdref := evd';
@@ -472,7 +474,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 		ctxt (Array.to_list l) (Id.Map.empty,[]) in
 	    (* Check if some rid to clear in the context of ev has dependencies
 	       in the type of ev and adjust the source of the dependency *)
-	    let nconcl =
+	    let _nconcl =
 	      try
                 let nids = Id.Map.domain rids in
                 check_and_clear_in_constr evdref (EvarTypingBreak ev) nids (evar_concl evi)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index fb52a0481..9157cdb81 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -159,9 +159,6 @@ let map_glob_constr_left_to_right f = function
       let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
       let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
       GCases (loc,sty,comp1,comp2,comp3)
-  | GProj (loc,p,c) -> 
-      let comp1 = f c in
-      GProj (loc,p,comp1)
   | GLetTuple (loc,nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
       let comp2 = f b in
@@ -189,7 +186,6 @@ let fold_glob_constr f acc =
   let rec fold acc = function
   | GVar _ -> acc
   | GApp (_,c,args) -> List.fold_left fold (fold acc c) args
-  | GProj (_,p,c) -> fold acc c
   | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) ->
       fold (fold acc b) c
   | GCases (_,_,rtntypopt,tml,pl) ->
@@ -228,7 +224,6 @@ let occur_glob_constr id =
   let rec occur = function
     | GVar (loc,id') -> Id.equal id id'
     | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
-    | GProj (loc,p,c) -> occur c
     | GLambda (loc,na,bk,ty,c) ->
       (occur ty) || (not (same_id na id) && (occur c))
     | GProd (loc,na,bk,ty,c) ->
@@ -278,7 +273,6 @@ let free_glob_vars  =
   let rec vars bounded vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
     | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GProj (loc,p,c) -> vars bounded vs c
     | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
 	let vs' = vars bounded vs ty in
 	let bounded' = add_name_to_ids bounded na in
@@ -340,7 +334,6 @@ let loc_of_glob_constr = function
   | GEvar (loc,_,_) -> loc
   | GPatVar (loc,_) -> loc
   | GApp (loc,_,_) -> loc
-  | GProj (loc,p,c) -> loc
   | GLambda (loc,_,_,_,_) -> loc
   | GProd (loc,_,_,_,_) -> loc
   | GLetIn (loc,_,_,_) -> loc
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 5828e7f43..54ce29bf7 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,8 +324,6 @@ let rec pat_of_raw metas vars = function
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
   | GApp (_, GPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | GProj (_, p, c) ->
-      PProj (p, pat_of_raw metas vars c)
   | GApp (_,c,cl) ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dfb6f80d9..93d65197b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -539,56 +539,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     let j = pretype_sort evdref s in
       inh_conv_coerce_to_tycon loc env evdref j tycon
 
-  | GProj (loc, p, arg) ->
-    let (cst, mind, n, m, ty) = 
-      try get_projection env p 
-      with Not_found ->
-	user_err_loc (loc,"",str "Not a projection")
-    in
-    let mk_ty k = 
-      let ind = 
-	Evarutil.evd_comb1 (Evd.fresh_inductive_instance env) evdref (mind,0)
-      in
-      let args = 
-	let ctx = smash_rel_context (Inductiveops.inductive_paramdecls ind) in
-	  List.fold_right (fun (n, b, ty) (* par  *)args ->
-	    let ty = substl args ty in
-	    let ev = e_new_evar env evdref ~src:(loc,k) ty in
-	      ev :: args) ctx []
-      in (ind, List.rev args)
-    in
-    let argtycon =
-      match arg with
-      | GHole (loc, k, _) -> (* Typeclass projection application: 
-				create the necessary type constraint *)
-	let ind, args = mk_ty k in
-	  mk_tycon (applist (mkIndU ind, args))
-      | _ -> empty_tycon
-    in
-    let recty = pretype argtycon env evdref lvar arg in
-    let recty, ((ind,u), pars) = 
-      try
-	let IndType (indf, _ (*[]*)) = 
-	  find_rectype env !evdref recty.uj_type
-	in 
-	let ((ind', _), _) as indf = dest_ind_family indf in
-	  if not (eq_ind ind' (mind,0)) then raise Not_found
-	  else recty, indf
-      with Not_found -> 
-	(match argtycon with
-	| Some ty -> assert false
-	| None -> 
-	  let ind, args = mk_ty Evar_kinds.InternalHole in
-	  let j' = 
-	    inh_conv_coerce_to_tycon (loc_of_glob_constr arg) env evdref recty 
-	      (mk_tycon (applist (mkIndU ind, args))) in
-	    j', (ind, args))
-    in
-    let ty = Vars.subst_instance_constr u ty in
-    let ty = substl (recty.uj_val :: List.rev pars) ty in
-    let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in
-      inh_conv_coerce_to_tycon loc env evdref j tycon
-
   | GApp (loc,f,args) ->
     let fj = pretype empty_tycon env evdref lvar f in
     let floc = loc_of_glob_constr f in
@@ -654,6 +604,17 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in
 	    let t = Retyping.get_type_of env !evdref c in
 	      make_judge c (* use this for keeping evars: resj.uj_val *) t
+	  else if isConst f then
+	    let c,_ = destConst f in (* Internalize as primitive projection *)
+	      if is_projection c env then
+		let pb = lookup_projection c env in 
+		let npars = pb.Declarations.proj_npars and argslen = Array.length args in
+		  if npars < argslen then
+		    let proj = mkProj (c, args.(npars)) in
+		    let args = Array.sub args (npars+1) (argslen - (npars + 1)) in
+		      make_judge (mkApp (proj,args)) resj.uj_type
+		  else resj
+	      else resj
 	  else resj
       | _ -> resj 
     in