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.

31 files changed, 225 insertions, 406 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2e6ab4354..b774da356 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -437,28 +437,14 @@ let occur_name na aty =
     | Name id -> occur_var_constr_expr id aty
     | Anonymous -> false
 
-let is_projection primprojapp nargs cf =
-  let env = Global.env () in
-    match primprojapp with 
-    | Some r ->
-      let pb = Environ.lookup_projection r env in
-	Some pb.Declarations.proj_npars, Some 1
-    | None ->
-      match cf with
-      | Some (ConstRef p) when Environ.is_projection p (Global.env()) ->
-	let pb = Environ.lookup_projection p env in
-        (* For primitive projections, r.(p) and r.(@p) are reserved to the 
-	   non-eta-expanded version of the constant, we disallow printing 
-	   of the eta-expanded projection as a projection *)
-	  Some pb.Declarations.proj_npars, None
-      | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
-	(try
-	   let n = Recordops.find_projection_nparams r + 1 in
-	     if n <= nargs then None, None
-	     else None, Some n
-	 with Not_found -> None, None)
-      | _ -> None, None
-      
+let is_projection nargs = function
+  | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
+    (try
+       let n = Recordops.find_projection_nparams r + 1 in
+	 if n <= nargs then None
+	 else Some n
+     with Not_found -> None)
+  | _ -> None
 	
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
@@ -481,7 +467,7 @@ let params_implicit n impl =
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize loc inctx impl (cf,primprojapp,f) args =
+let explicitize loc inctx impl (cf,f) args =
   let impl = if !Constrintern.parsing_explicit then [] else impl in
   let n = List.length args in
   let rec exprec q = function
@@ -506,44 +492,27 @@ let explicitize loc inctx impl (cf,primprojapp,f) args =
       raise Expl
     | [], _ -> []
   in
-  let primproj, ip = is_projection primprojapp (List.length args) cf in
+  let ip = is_projection (List.length args) cf in
   let expl () = 
     match ip with
     | Some i ->
-      (match primproj with
-      | Some npars -> (* Primitive projection in projection notation *)
-	let projimpl = CList.skipn_at_least npars impl in
-	  if not !print_projections && not !Flags.raw_print && params_implicit npars impl then
-	    (* Printing primitive projection as application *)
-	    let args = exprec 1 (args,projimpl) in		  
-	      CApp (loc, (None, f), args)
-	  else (** Printing as projection *)
-	    let args = exprec 1 (args,projimpl) in
-	      CApp (loc, (Some i,f),args)
-      | None -> (** Regular constant in projection notation *)
-	if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
-	  raise Expl
-	else
-	  let (args1,args2) = List.chop i args in
-	  let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
-	  let args1 = exprec 1 (args1,impl1) in
-	  let args2 = exprec (i+1) (args2,impl2) in
-	  let ip = Some (List.length args1) in
-	    CApp (loc,(ip,f),args1@args2))
-    | None ->
-      match primproj with
-      | Some npars when List.length args > npars && params_implicit npars impl ->
-        (* Eta-expanded version of projection, print explicited if the implicit 
-	   application would be parsed as a primitive projection application. *)
+      if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
 	raise Expl
-      | _ -> 
-        let args = exprec 1 (args,impl) in
-	  if List.is_empty args then f else CApp (loc, (None, f), 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
+	let args1 = exprec 1 (args1,impl1) in
+	let args2 = exprec (i+1) (args2,impl2) in
+	let ip = Some (List.length args1) in
+	  CApp (loc,(ip,f),args1@args2)
+    | None ->
+      let args = exprec 1 (args,impl) in
+	if List.is_empty args then f else CApp (loc, (None, f), args)
   in
     try expl ()
     with Expl -> 
       let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
-      let ip = if primprojapp != None || !print_projections then ip else None in
+      let ip = if !print_projections then ip else None in
 	CAppExpl (loc, (ip, f', us), args)
 
 let is_start_implicit = function
@@ -557,7 +526,7 @@ let extern_global loc impl f us =
   else
     CRef (f,us)
 
-let extern_app loc inctx impl (cf,primproj,f) us args =
+let extern_app loc inctx impl (cf,f) us args =
   if List.is_empty args then
     (* If coming from a notation "Notation a := @b" *)
     CAppExpl (loc, (None, f, us), [])
@@ -566,12 +535,9 @@ let extern_app loc inctx impl (cf,primproj,f) us args =
       (!print_implicits && not !print_implicits_explicit_args)) &&
      List.exists is_status_implicit impl)
   then
-    if primproj != None then
-      CAppExpl (loc, (Some 1,f,us), args)
-    else
-      CAppExpl (loc, (snd (is_projection primproj (List.length args) cf),f,us), args)
+    CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
   else
-    explicitize loc inctx impl (cf,primproj,CRef (f,us)) args
+    explicitize loc inctx impl (cf,CRef (f,us)) args
 
 let rec extern_args extern scopes env args subscopes =
   match args with
@@ -585,12 +551,6 @@ let rec extern_args extern scopes env args subscopes =
 
 let match_coercion_app = function
   | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
-  | GProj (loc, r, arg) -> 
-    let pars = Inductiveops.projection_nparams r in
-      Some (loc, ConstRef r, pars, [arg])
-  | GApp (loc,GProj (_, r, c), args) -> 
-    let pars = Inductiveops.projection_nparams r in
-      Some (loc, ConstRef r, pars, c :: args)
   | _ -> None
 
 let rec remove_coercions inctx c =
@@ -728,27 +688,13 @@ let rec extern inctx scopes vars r =
 		 | Not_found | No_match | Exit ->
 		     extern_app loc inctx
 		       (select_stronger_impargs (implicits_of_global ref))
-		       (Some ref,None,extern_reference rloc vars ref) (extern_universes us) args
+		       (Some ref,extern_reference rloc vars ref) (extern_universes us) args
 	     end
-
-	 | GProj (loc,p,c) ->
-	   let ref = ConstRef p in
-	   let subscopes = find_arguments_scope ref in
-	   let args =
-	     extern_args (extern true) (snd scopes) vars (c :: args) subscopes 
-	   in
-	     extern_app loc inctx 
-	     (select_stronger_impargs (implicits_of_global ref))
-	       (Some ref, Some p, extern_reference loc vars ref)
-	       None args
 	       
 	 | _       ->
-	   explicitize loc inctx [] (None,None,sub_extern false scopes vars f)
+	   explicitize loc inctx [] (None,sub_extern false scopes vars f)
              (List.map (sub_extern true scopes vars) args))
 
-  | GProj (loc,p,c) ->
-    extern inctx scopes vars (GApp (loc,r',[]))
-
   | GLetIn (loc,na,t,c) ->
       CLetIn (loc,(loc,na),sub_extern false scopes vars t,
               extern inctx scopes (add_vname vars na) c)
@@ -967,7 +913,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
  	if List.is_empty args then e
 	else
 	  let args = extern_args (extern true) scopes vars args argsscopes in
-	  explicitize loc false argsimpls (None,None,e) args
+	  explicitize loc false argsimpls (None,e) args
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
@@ -989,7 +935,7 @@ let extern_glob_type vars c =
 
 let loc = Loc.ghost (* for constr and pattern, locations are lost *)
 
-let extern_constr_gen goal_concl_style scopt env sigma t =
+let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -998,21 +944,19 @@ let extern_constr_gen goal_concl_style scopt env sigma t =
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then ids_of_context env else [] in
-  let rel_env_names = names_of_rel_context env in
-  let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in
+  let r = Detyping.detype ~lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
 
 let extern_constr_in_scope goal_concl_style scope env sigma t =
-  extern_constr_gen goal_concl_style (Some scope) env sigma t
+  extern_constr_gen false goal_concl_style (Some scope) env sigma t
 
-let extern_constr goal_concl_style env sigma t =
-  extern_constr_gen goal_concl_style None env sigma t
+let extern_constr ?(lax=false) goal_concl_style env sigma t =
+  extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
   let avoid = if goal_concl_style then ids_of_context env else [] in
-  let rel_env_names = names_of_rel_context env in
-  let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in
+  let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort s = extern_glob_sort (detype_sort s)
@@ -1076,14 +1020,14 @@ let rec glob_of_pat env sigma = function
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> Detyping.detype false [] env sigma (mkFix f)
-  | PCoFix c -> Detyping.detype false [] env sigma (mkCoFix c)
+  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *)
+  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c)
   | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
-  let a = detype_rel_context where [] (names_of_rel_context env) sigma sign in
+  let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index a994d8693..023c5be22 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -30,9 +30,12 @@ val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
-   level of quantification clashing with the variables in [env] are renamed *)
+   level of quantification clashing with the variables in [env] are renamed.
+    ~lax is for debug printing, when the constr might not be well typed in 
+    env, sigma
+*)
 
-val extern_constr : bool -> env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 66f51b19e..56780e240 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
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c69eb629d..90303cc92 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -127,7 +127,6 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
 	  else (id, loc) :: vs
 	else vs
     | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GProj (loc,p,c) -> vars bound vs c
     | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
 	let vs' = vars bound vs ty in
 	let bound' = add_name_to_ids bound na in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 1aac1c53d..81e2ac810 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -55,7 +55,6 @@ let ldots_var = Id.of_string ".."
 let glob_constr_of_notation_constr_with_binders loc g f e = function
   | NVar id -> GVar (loc,id)
   | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
-  | NProj (p,c) -> GProj (loc,p,f e c)
   | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
       let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in
@@ -150,7 +149,6 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
   | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
-  | GProj (_,p1,c1), GProj (_, p2, c2) -> eq_constant p1 p2 && f c1 c2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
     on_true_do (f ty1 ty2 && f c1 c2) add na1
@@ -166,7 +164,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | _,(GCases _ | GRec _
       | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
       -> error "Unsupported construction in recursive notations."
-  | (GRef _ | GVar _ | GApp _ | GProj _ | GLambda _ | GProd _
+  | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
     | GHole _ | GSort _ | GLetIn _), _
       -> false
 
@@ -261,7 +259,6 @@ let notation_constr_and_vars_of_glob_constr a =
   and aux' = function
   | GVar (_,id) -> add_id found id; NVar id
   | GApp (_,g,args) -> NApp (aux g, List.map aux args)
-  | GProj (_,p,c) -> NProj (p, aux c)
   | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
   | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
   | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c)
@@ -356,7 +353,7 @@ let notation_constr_of_glob_constr nenv a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
-  let t = Detyping.detype false avoiding [] Evd.empty t in
+  let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
@@ -388,12 +385,6 @@ let rec subst_notation_constr subst bound raw =
 	if r' == r && rl' == rl then raw else
 	  NApp(r',rl')
 
-  | NProj (p,c) ->
-      let p' = subst_constant subst p in
-      let c' = subst_notation_constr subst bound c in
-	if p == p' && c == c' then raw else
-	  NProj (p',c')
-
   | NList (id1,id2,r1,r2,b) ->
       let r1' = subst_notation_constr subst bound r1
       and r2' = subst_notation_constr subst bound r2 in
@@ -669,8 +660,6 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
   | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
   | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma
-  | GProj (loc,f1,c1), NProj (f2,c2) when Constant.equal f1 f2 -> 
-     match_in u alp metas sigma c1 c2
   | GApp (loc,f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 33c21eea5..bb4109009 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -108,7 +108,7 @@ let constr_key c =
 let revert_reserved_type t =
   try
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
-    let t = Detyping.detype false [] [] Evd.empty t in
+    let t = Detyping.detype false [] (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 237d03366..832ee4e4b 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -41,7 +41,6 @@ type glob_constr =
   | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses
       (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
 	  [MatchStyle]) *)
-  | GProj of Loc.t * projection * glob_constr
   | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) *
       glob_constr * glob_constr
   | GIf of Loc.t * glob_constr * (Name.t * glob_constr option) * glob_constr * glob_constr
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 8bb43e96a..daf605ab2 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -25,7 +25,6 @@ type notation_constr =
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
   | NHole of Evar_kinds.t * Genarg.glob_generic_argument option
-  | NProj of projection * notation_constr
   | NList of Id.t * Id.t * notation_constr * notation_constr * bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 10d1b6314..e77ba3c58 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -316,7 +316,7 @@ let rec match_aliases names constr = function
       let args,bnames,body = match_aliases qnames body q in
 	st::args,bnames,body
 
-let detype_ground c = Detyping.detype false [] [] Evd.empty c
+let detype_ground env c = Detyping.detype false [] env Evd.empty c
 
 let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
@@ -334,7 +334,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
 	     str "expected.") in
   let app_ind =
     let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
-    let rparams = List.map detype_ground pinfo.per_params in
+    let rparams = List.map (detype_ground env) pinfo.per_params in
     let rparams_rec =
       List.map
 	(fun (loc,(id,_)) ->
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 422b7c499..a5f28003c 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1272,8 +1272,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 
 let understand_my_constr c gls =
   let env = pf_env gls in
-  let nc = names_of_rel_context env in
-  let rawc = Detyping.detype false [] nc Evd.empty c in
+  let rawc = Detyping.detype false [] env Evd.empty c in
   let rec frob = function
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None)
     | rc ->  map_glob_constr frob rc
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2987ce60a..80576212f 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t=
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] [] evmap nt in
+  let rawt=Detyping.detype false [] env evmap nt in
   let rec raux n t=
     if Int.equal n 0 then t else
       match t with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6d2274365..4f308af5e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty csta.(i))
+	     (fun i -> Detyping.detype false [] env Evd.empty csta.(i))
 	  )
       in
       let patl_as_term =
@@ -488,7 +488,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in
 		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
-		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty rt_typ in
+		let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -559,7 +559,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		build_entry_lc env funnames avoid (mkGApp(b,args))
 	    | GRec _ -> error "Not handled GRec"
-            | GProj _ -> error "Not handled GProj"
 	    | GProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *)
 
@@ -662,7 +661,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 
 	end
     | GRec _ -> error "Not handled GRec"
-    | GProj _ -> error "Not handled GProj"
     | GCast(_,b,_) ->
 	build_entry_lc env funnames  avoid b
 and build_entry_lc_from_case env funname make_discr
@@ -743,7 +741,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
-			    (Termops.names_of_rel_context env_with_pat_ids) Evd.empty typ_of_id
+			    env_with_pat_ids Evd.empty typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
 		     pat_ids
@@ -787,7 +785,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
-		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_as_constr in
+		 let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
 		   (fun id  acc ->
@@ -795,7 +793,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_of_id
+			Detyping.detype false [] new_env Evd.empty typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -951,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
-				 (Termops.names_of_rel_context env) Evd.empty
+				 env Evd.empty
 				 p) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
@@ -979,12 +977,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				     | Anonymous -> acc
 				     | Name id' ->
 					 (id',Detyping.detype false []
-					    (Termops.names_of_rel_context env)
+					    env
                                             Evd.empty
 					    arg)::acc
 				 else if isVar var_as_constr
 				 then (destVar var_as_constr,Detyping.detype false []
-					 (Termops.names_of_rel_context env)
+					 env
                                          Evd.empty
 					 arg)::acc
 				 else acc
@@ -1183,7 +1181,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ | GProj _->
+  | GIf _ | GRec _ | GCast _ ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 4cdea414e..e55ede968 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -180,7 +180,6 @@ let change_vars =
       | GRec _ -> error "Local (co)fixes are not supported"
       | GSort _ -> rt
       | GHole _ -> rt
-      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GCast(loc,b,c) ->
 	  GCast(loc,change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
@@ -358,7 +357,6 @@ let rec alpha_rt excluded rt =
 	    alpha_rt excluded rhs
 	   )
     | GRec _ -> error "Not handled GRec"
-    | GProj _ -> error "Native projections are not supported" (** FIXME *)
     | GSort _ -> rt
     | GHole _ -> rt
     | GCast (loc,b,c) ->
@@ -409,7 +407,6 @@ let is_free_in id =
     | GIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
     | GRec _ -> raise (UserError("",str "Not handled GRec"))
-    | GProj _ -> error "Native projections are not supported" (** FIXME *)
     | GSort _ -> false
     | GHole _ -> false
     | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -506,7 +503,6 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern rhs
 	     )
       | GRec _ -> raise (UserError("",str "Not handled GRec"))
-      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
@@ -602,7 +598,6 @@ let ids_of_glob_constr c =
       | GCases (loc,sty,rtntypopt,tml,brchl) ->
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
       | GRec _ -> failwith "Fix inside a constructor branch"
-      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
   (* build the set *)
@@ -661,7 +656,6 @@ let zeta_normalize =
 	      zeta_normalize_term rhs
 	     )
       | GRec _ -> raise (UserError("",str "Not handled GRec"))
-      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
@@ -704,7 +698,6 @@ let expand_as =
 	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | GRec _ ->  error "Not handled GRec"
-      | GProj _ -> error "Native projections are not supported" (** FIXME *)
       | GCast(loc,b,c) ->
 	  GCast(loc,expand_as map b,
 		Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index cd35a09a1..be84f2ed4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -181,7 +181,6 @@ let is_rec names =
   let rec lookup names = function
     | GVar(_,id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
-    | GProj (loc, p, c) -> lookup names c
     | GCast(_,b,_) -> lookup names b
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 669b77e03..8e3c0ba9c 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -773,7 +773,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
-    Detyping.detype false (Id.Set.elements avoid) [] Evd.empty substindtyp in
+    Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
@@ -854,7 +854,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
 let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
-        let traw = Detyping.detype false [] [] Evd.empty t in
+        let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
         GProd (Loc.ghost,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false
 
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
diff --git a/printing/printer.ml b/printing/printer.ml
index 3264c93a5..c83a9fb04 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -138,7 +138,8 @@ let pr_constr_pattern t =
 
 let pr_sort s = pr_glob_sort (extern_sort s)
 
-let _ = Termops.set_print_constr (fun env -> pr_lconstr_env env Evd.empty)
+let _ = Termops.set_print_constr 
+  (fun env t -> pr_lconstr_expr (extern_constr ~lax:true false env Evd.empty t))
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 let pr_univ_cstr (c:Univ.constraints) =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e4ba9a7ee..41f8dc8de 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -628,9 +628,8 @@ let hResolve id c occ t gl =
   let sigma = project gl in 
   let env = Termops.clear_named_body id (pf_env gl) in
   let env_ids = Termops.ids_of_context env in
-  let env_names = Termops.names_of_rel_context env in
-  let c_raw = Detyping.detype true env_ids env_names sigma c in
-  let t_raw = Detyping.detype true env_ids env_names sigma t in
+  let c_raw = Detyping.detype true env_ids env sigma c in
+  let t_raw = Detyping.detype true env_ids env sigma t in
   let rec resolve_hole t_hole =
     try 
       Pretyping.understand env sigma t_hole
diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index 43108ab4b..ca4d23803 100644
--- a/test-suite/bugs/closed/3454.v
+++ b/test-suite/bugs/closed/3454.v
@@ -1,8 +1,11 @@
 Set Primitive Projections.
 Set Implicit Arguments.
+
+Record prod {A} {B}:= pair { fst : A ; snd : B }.
+Notation " A * B " := (@prod A B) : type_scope.
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 Notation pr1 := (@projT1 _ _).
-
+Arguments prod : clear implicits.
 
 Check (@projT1 _ (fun x : nat => x = x)).
 Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).
@@ -13,7 +16,7 @@ Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
 Check (fun r : @rimpl true 0 => @foo true 0 r 0).
 Check (fun r : @rimpl true 0 => foo r (x:=0)).
 Check (fun r : @rimpl true 0 => @foo _ _ r 0).
-Check (fun r : @rimpl true 0 => r.(@foo)).
+Check (fun r : @rimpl true 0 => r.(@foo _ _)).
 Check (fun r : @rimpl true 0 => r.(foo)).
 
 Notation "{ x : T  & P }" := (@sigT T P).
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index b47bb3a20..c68796593 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
 Inductive Empty : Prop := .
 
 Inductive paths {A : Type} (a : A) : A -> Type :=
@@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inl y' => ap g
                          | inr y' => idmap
                        end
-           | inr x' => match y as y return match y return Type with
+           | inr x' => match y as y return match y return Prop with
                                                inr y' => x' = y'
                                              | _ => Empty
-                                           end -> match f y return Type with
+                                           end -> match f y return Prop with
                                                     | inr y' => h x' = y'
                                                     | _ => Empty end with
                          | inl y' => idmap
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index 77f921b7c..cc3048027 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -115,7 +115,7 @@ Section path_functor.
   Proof.
     intros [H' H''].
     destruct F, G; simpl in *.
-    induction H'; induction H''; simpl.
+    induction H'. (* while destruct H' works *) destruct H''.
     apply ap11; [ apply ap | ];
     apply center; abstract exact _.
     Set Printing Universes.
diff --git a/test-suite/bugs/opened/HoTT_coq_083.v b/test-suite/bugs/opened/HoTT_coq_083.v
deleted file mode 100644
index 091720272..000000000
--- a/test-suite/bugs/opened/HoTT_coq_083.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record category :=
-  { ob : Type }.
-
-Goal forall C, ob C -> ob C.
-intros.
-generalize dependent (ob C).
-(* 1 subgoals, subgoal 1 (ID 7)
-
-  C : category
-  ============================
-   forall T : Type, T -> T
-(dependent evars:) *)
-intros T t.
-Undo 2.
-generalize dependent (@ob C).
-(* 1 subgoals, subgoal 1 (ID 6)
-
-  C : category
-  X : ob C
-  ============================
-   Type -> ob C
-(dependent evars:) *)
-Fail intros T t.
-(* Toplevel input, characters 9-10:
-Error: No product even after head-reduction. *)
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 74083ac89..068f8ac3c 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -115,22 +115,22 @@ Unset Printing All.
 
 (** Explicit version of the primitive projection, under applied w.r.t implicit arguments
       can be printed only using projection notation. r.(@p) *)
-Check r.(@p). 
+Check r.(@p _). 
 Set Printing Projections.
-Check r.(@p). 
+Check r.(@p _). 
 Unset Printing Projections.
 Set Printing All.
-Check r.(@p).
+Check r.(@p _).
 Unset Printing All.
   
 (** Explicit version of the primitive projection, applied to its implicit arguments
       can be printed using application notation r.(p), r.(@p) in fully explicit form *)
-Check r.(@p) nat.
+Check r.(@p _) nat.
 Set Printing Projections.
-Check r.(@p) nat. 
+Check r.(@p _) nat. 
 Unset Printing Projections.
 Set Printing All.
-Check r.(@p) nat.
+Check r.(@p _) nat.
 Unset Printing All.
 
 Parameter r' : R' nat.
@@ -163,12 +163,12 @@ Unset Printing All.
 
 (** Explicit version of the primitive projection, under applied w.r.t implicit arguments
       can be printed only using projection notation. r.(@p) *)
-Check r'.(@p'). 
+Check r'.(@p' _). 
 Set Printing Projections.
-Check r'.(@p'). 
+Check r'.(@p' _). 
 Unset Printing Projections.
 Set Printing All.
-Check r'.(@p').
+Check r'.(@p' _).
 Unset Printing All.
   
 (** Explicit version of the primitive projection, applied to its implicit arguments
@@ -181,3 +181,10 @@ Set Printing All.
 Check p' r' nat. 
 Unset Printing All.
 
+Check (@p' nat).
+Check p'.
+Set Printing All.
+
+Check (@p' nat).
+Check p'.
+Unset Printing All.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 490addddb..9aa43bd42 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1116,8 +1116,9 @@ let default_env () = {
 
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
-    let t,ctx = Constrintern.interp_type (Global.env()) Evd.empty c in
-    let t = Detyping.detype false [] [] Evd.empty t in
+    let env = Global.env() in
+    let t,ctx = Constrintern.interp_type env Evd.empty c in
+    let t = Detyping.detype false [] env Evd.empty t in
     let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index c167f9b79..f07d31505 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -144,7 +144,6 @@ let rec uri_of_constr c =
   | GRef (_,ref,_) ->  uri_of_global ref
   | GHole _ | GEvar _ -> url_string "?"
   | GSort (_,s) -> url_string (whelp_of_glob_sort s)
-  | GProj _ -> assert false
   | GApp (_,f,args) ->
       let inst,rest = merge (section_parameters f) args in
       uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
@@ -176,14 +175,14 @@ let send_whelp req s =
   let command = Util.subst_command_placeholder browser_cmd_fmt url in
   let _ = CUnix.run_command ~hook:print_string command in ()
 
-let whelp_constr req c =
-  let c = detype false [whelm_special] [] Evd.empty c in
+let whelp_constr env sigma req c =
+  let c = detype false [whelm_special] env sigma c in
   send_whelp req (make_string uri_of_constr c)
 
 let whelp_constr_expr req c =
   let (sigma,env)= Lemmas.get_current_context () in
   let _,c = interp_open_constr env sigma c in
-  whelp_constr req c
+  whelp_constr env sigma req c
 
 let whelp_locate s =
   send_whelp "locate" s
@@ -194,7 +193,7 @@ let whelp_elim ind =
 let on_goal f =
   let gls = Proof.V82.subgoals (get_pftreestate ()) in
   let gls = { gls with Evd.it = List.hd gls.Evd.it }  in
-  f (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
+  f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
 
 type whelp_request =
   | Locate of string
@@ -204,7 +203,7 @@ type whelp_request =
 let whelp = function
   | Locate s -> whelp_locate s
   | Elim ind -> whelp_elim ind
-  | Constr (s,c) -> whelp_constr s c
+  | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c
 
 VERNAC ARGUMENT EXTEND whelp_constr_request
 | [ "Match" ] -> [ "match" ]
@@ -221,5 +220,5 @@ END
 VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY
 | [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ]
 | [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] ->
-  [ on_goal (whelp_constr "hint") ]
+  [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ]
 END