Fix debug printing with primitive projections.

Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.

3 files changed, 12 insertions, 11 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 823f5ef644..d691acb45f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -438,15 +438,14 @@ let rec detype flags avoid env sigma t =
 	  (Array.map_to_list (detype flags avoid env sigma) args)
     | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
     | Proj (p,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)
+      if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
+	(* lax mode, used by debug printers only *) 
+	GApp (dl, GRef (dl, ConstRef p, None), 
+	      [detype flags avoid env sigma c])
+      else 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]))
     | Evar (evk,cl) ->
       let id,l =
         try Evd.evar_ident evk sigma,
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index c7bdabe93f..8f1a16dce3 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,8 +126,9 @@ let retype ?(polyprop=true) sigma =
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Proj (p,c) -> 
        let Inductiveops.IndType(pars,realargs) =
-         try Inductiveops.find_rectype env sigma (type_of env c)
-         with Not_found -> anomaly ~label:"type_of" (str "Bad recursive type") 
+	 let ty = type_of env c in
+           try Inductiveops.find_rectype env sigma ty
+           with Not_found -> retype_error BadRecursiveType
        in
        let (_,u), pars = dest_ind_family pars in
 	 substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7b302229bc..d03fd85211 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1325,6 +1325,7 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) =
     with
     | PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
         raise (NotUnifiable (Some (c1,c2,e)))
+    (** MS: This is pretty bad, it catches Not_found for example *)
     | e when Errors.noncritical e -> raise (NotUnifiable None) in
   let merge_fun c1 c2 =
     match c1, c2 with