Delayed the evar normalization in error messages to the last minute

before the message is delivered to the user. Should avoid useless
computation in heavily backtracking tactics (auto, try, ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 141 insertions, 133 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7b1fba011..7af0a357a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -57,7 +57,7 @@ let ppsconstr x = ppconstr (Declarations.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let pprawconstr = (fun x -> pp(pr_lrawconstr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
-let pptype = (fun x -> pp(pr_ltype x))
+let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
 
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 4a244553e..62fa0b2c9 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -218,7 +218,7 @@ let subtac (loc, command) =
 
   | Type_errors.TypeError (env, exn) as e -> raise e
 
-  | Pretype_errors.PretypeError (env, exn) as e -> raise e
+  | Pretype_errors.PretypeError (env, _, exn) as e -> raise e
 
   | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
      Loc.Exc_located (loc, e') as e) -> raise e
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index eb07addb0..cd2ed76c1 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -38,8 +38,9 @@ type pretype_error =
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
   | Util.UserError _ | TypeError _ | PretypeError _
@@ -55,13 +56,13 @@ let j_nf_betaiotaevar sigma j =
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = Reductionops.nf_betaiota sigma j.uj_type }
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jl_nf_betaiotaevar sigma jl =
-  List.map (j_nf_betaiotaevar sigma) jl
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar sigma) jl
 let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=nf_evar sigma v;utj_type=t}
 
-let env_ise sigma env =
+let env_nf_evar sigma env =
   let sign = named_context_val env in
   let ctxt = rel_context env in
   let env0 = reset_with_named_context sign env in
@@ -97,110 +98,90 @@ let contract2 env a b = match contract env [a;b] with
 let contract3 env a b c = match contract env [a;b;c] with
   | env, [a;b;c] -> env,a,b,c | _ -> assert false
 
-let raise_pretype_error (loc,ctx,sigma,te) =
-  Loc.raise loc (PretypeError(env_ise sigma ctx,te))
+let raise_pretype_error (loc,env,sigma,te) =
+  Loc.raise loc (PretypeError(env,sigma,te))
 
-let raise_located_type_error (loc,ctx,sigma,te) =
-  Loc.raise loc (TypeError(env_ise sigma ctx,te))
+let raise_located_type_error (loc,env,sigma,te) =
+  Loc.raise loc (PretypeError(env,sigma,TypingError te))
 
 
 let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
   let env, c, actty, expty = contract3 env c actty expty in
-  let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in
-  raise_located_type_error
-    (loc, env, sigma, ActualType (j, nf_evar sigma expty))
+  let j = {uj_val=c;uj_type=actty} in
+  raise_located_type_error (loc, env, sigma, ActualType (j, expty))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
-  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, env, sigma,
-    CantApplyNonFunctional (j_nf_evar sigma rator, ja))
+    (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
 
 let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
-  let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in
   raise_located_type_error
     (loc, env, sigma,
-     CantApplyBadType
-       ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t),
-        j_nf_evar sigma rator, ja))
+       CantApplyBadType ((n,c,t), rator, Array.of_list randl))
 
 let error_ill_formed_branch_loc loc env sigma c i actty expty =
-  let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
   raise_located_type_error
-    (loc, env, sigma,
-     IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
+    (loc, env, sigma, IllFormedBranch (c, i, actty, expty))
 
 let error_number_branches_loc loc env sigma cj expn =
-  raise_located_type_error
-    (loc, env, sigma,
-     NumberBranches (j_nf_evar sigma cj, expn))
+  raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn))
 
 let error_case_not_inductive_loc loc env sigma cj =
-  raise_located_type_error
-    (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
+  raise_located_type_error (loc, env, sigma, CaseNotInductive cj)
 
 let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
   raise_located_type_error
-    (loc, env, sigma,
-     IllTypedRecBody (i,na,jv_nf_evar sigma jl,
-                      Array.map (nf_evar sigma) tys))
+    (loc, env, sigma, IllTypedRecBody (i, na, jl, tys))
 
 let error_not_a_type_loc loc env sigma j =
-  raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j))
+  raise_located_type_error (loc, env, sigma, NotAType j)
 
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
 
 let error_occur_check env sigma ev c =
-  let c = nf_evar sigma c in
-  raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
+  raise (PretypeError (env, sigma, OccurCheck (ev,c)))
 
 let error_not_clean env sigma ev c (loc,k) =
-  let c = nf_evar sigma c in
-  Loc.raise loc
-    (PretypeError (env_ise sigma env,  NotClean (ev,c,k)))
+  Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
 
 let error_unsolvable_implicit loc env sigma evi e explain =
   Loc.raise loc
-    (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain)))
+    (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
 
 let error_cannot_unify env sigma (m,n) =
-  let m = nf_evar sigma m and n = nf_evar sigma n in
-  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
-  raise (PretypeError (env_ise sigma env,CannotUnifyLocal (m,n,sn)))
+  raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
 
 let error_cannot_coerce env sigma (m,n) =
-  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_find_well_typed_abstraction env sigma p l =
-  raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+  raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
 
 let error_abstraction_over_meta env sigma hdmeta metaarg =
   let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
-  raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n)))
+  raise (PretypeError (env, sigma,AbstractionOverMeta (m,n)))
 
 let error_non_linear_unification env sigma hdmeta t =
   let m = Evd.meta_name sigma hdmeta in
-  raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t)))
+  raise (PretypeError (env, sigma,NonLinearUnification (m,t)))
 
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
-  raise_pretype_error
-    (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
+  raise_pretype_error (loc, env, sigma, CantFindCaseType expr)
 
 (*s Pretyping errors *)
 
 let error_unexpected_type_loc loc env sigma actty expty =
   let env, actty, expty = contract2 env actty expty in
-  raise_pretype_error
-    (loc, env, sigma,
-     UnexpectedType (nf_evar sigma actty, nf_evar sigma expty))
+  raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty))
 
 let error_not_product_loc loc env sigma c =
-  raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c))
+  raise_pretype_error (loc, env, sigma, NotProduct c)
 
 (*s Error in conversion from AST to rawterms *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index d81adb6b0..cdf6b523c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -37,47 +37,48 @@ type pretype_error =
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of Type_errors.type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 val precatchable_exception : exn -> bool
 
 (** Presenting terms without solved evars *)
-val nf_evar :  Evd.evar_map -> constr -> constr
-val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
-   Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
-   Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
-   Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+val nf_evar : Evd.evar_map -> constr -> constr
+val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
+val env_nf_evar : Evd.evar_map -> env -> env
+val jv_nf_betaiotaevar :
+  Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 
 (** Raising errors *)
 val error_actual_type_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> constr -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
 
 val error_cant_apply_not_functional_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_cant_apply_bad_type_loc :
-  loc -> env ->  Evd.evar_map -> int * constr * constr ->
+  loc -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
 val error_case_not_inductive_loc :
-  loc -> env ->  Evd.evar_map -> unsafe_judgment -> 'b
+  loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_ill_formed_branch_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       constr -> int -> constr -> constr -> 'b
 
 val error_number_branches_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body_loc :
-  loc -> env ->  Evd.evar_map ->
+  loc -> env -> Evd.evar_map ->
       int -> name array -> unsafe_judgment array -> types array -> 'b
 
 val error_not_a_type_loc :
@@ -87,7 +88,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
 (** {6 Implicit arguments synthesis errors } *)
 
-val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
+val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_not_clean :
   env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
@@ -112,15 +113,15 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type_loc :
-  loc -> env ->  Evd.evar_map -> constr -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product_loc :
-  loc -> env ->  Evd.evar_map -> constr -> 'b
+  loc -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to rawterms } *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 38cf59bc0..6c17567c3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -844,7 +844,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
-    raise (PretypeError (env,NoOccurrenceFound (op, None)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
 
 (* Tries to find all instances of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] and return all the matches.
@@ -906,7 +906,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
   in
   let res = matchrec cl [] in
   if res = [] then
-    raise (PretypeError (env,NoOccurrenceFound (op, None)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
   else
     res
 
@@ -922,7 +922,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
-	  with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
         in
 	  if not allow_K && (* ensure we found a different instance *)
 	    List.exists (fun op -> eq_constr op cl) l
@@ -932,7 +932,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
 	(evd,op::l)
       else
 	(* This is not up to delta ... *)
-	raise (PretypeError (env,NoOccurrenceFound (op, None))))
+	raise (PretypeError (env,evd,NoOccurrenceFound (op, None))))
     oplist
     (evd,[])
 
@@ -996,13 +996,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 	    with ex when precatchable_exception ex ->
 	      try
 		w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	      with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
+	      with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
 
       (* Second order case *)
       | (Meta _, true, _, _ | _, _, Meta _, true) ->
 	  (try
 	      w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	    with PretypeError (env,NoOccurrenceFound _) as e -> raise e
+	    with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
 	      | ex when precatchable_exception ex ->
 		  try
 		    w_typed_unify env cv_pb flags ty1 ty2 evd
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 70f2f6b64..71d952caf 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -448,7 +448,7 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,NotClean _) as e -> raise e
+      | PretypeError (_,_,NotClean _) as e -> raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 593ef0b32..5b55e1c02 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -48,13 +48,13 @@ open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
   | LtacLocated(_,e) -> catchable_exception e
-  | Util.UserError _ | TypeError _
+  | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
   | RefinerError _ | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* reduction errors *)
   | Tacred.ReductionTacticError _ 
   (* unification errors *)
-  | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+  | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _|OccurCheck _
 		   |UnsolvableImplicit _)) -> true
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 677c73942..2802acfc1 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -395,11 +395,12 @@ let rec tclGOALBINDU s k =
 open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
-  | Util.UserError _ | Type_errors.TypeError _ 
+  | Util.UserError _
+  | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
   | Indrec.RecursionSchemeError _
-  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
+  | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
   (* unification errors *)
-  | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+  | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ed754f6f..0144fbb34 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -134,10 +134,10 @@ let general_elim_clause with_evars cls rew elim =
              an extra condition *)
 	  tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false)
       | Some id -> rewrite_elim_in with_evars id rew elim)
-  with Pretype_errors.PretypeError (env,
-				   (Pretype_errors.NoOccurrenceFound (c', _))) ->
+  with Pretype_errors.PretypeError (env,evd,
+				    Pretype_errors.NoOccurrenceFound (c', _)) ->
     raise (Pretype_errors.PretypeError
-	      (env, (Pretype_errors.NoOccurrenceFound (c', cls))))
+	      (env,evd,Pretype_errors.NoOccurrenceFound (c', cls)))
 
 let general_elim_clause with_evars tac cls sigma c t l l2r elim gl =
   let all, firstonly, tac =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0490f1bc8..f9c8e47fd 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -578,7 +578,7 @@ let hResolve id c occ t gl =
     try 
       Pretyping.Default.understand sigma env t_hole
     with 
-    | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+    | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) ->
         resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 99cbfe498..860f162db 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1532,7 +1532,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
     with RewriteFailure ->
       let {l2r=l2r; c1=x; c2=y} = hypinfo in
 	raise (Pretype_errors.PretypeError
-		  (pf_env gl,
+		  (pf_env gl,project gl,
 		  Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl)))
 
 let general_s_rewrite_clause x =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d18b540de..2c4201f99 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -787,9 +787,9 @@ let simplest_elim c = default_elim false (c,NoBindings)
 
 let clenv_fchain_in id elim_flags mv elimclause hypclause =
   try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause
-  with PretypeError (env,NoOccurrenceFound (op,_)) ->
+  with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
     (* Set the hypothesis name in the message *)
-    raise (PretypeError (env,NoOccurrenceFound (op,Some id)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
 
 let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 68483f5e2..a497aad59 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -103,9 +103,9 @@ let rec process_vernac_interp_error = function
 	  mt() in
       wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error (Himsg.explain_type_error ctx te)
-  | PretypeError(ctx,te) ->
-      wrap_vernac_error (Himsg.explain_pretype_error ctx te)
+      wrap_vernac_error (Himsg.explain_type_error ctx Evd.empty te)
+  | PretypeError(ctx,sigma,te) ->
+      wrap_vernac_error (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
       wrap_vernac_error (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 191014c0b..01eca8cb2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -50,7 +50,8 @@ let explain_unbound_var env v =
   let var = pr_id v in
   str "No such section variable or assumption: " ++ var ++ str "."
 
-let explain_not_type env j =
+let explain_not_type env sigma j =
+  let j = j_nf_evar sigma j in
   let pe = pr_ne_context_of (str "In environment") env in
   let pc,pt = pr_ljudge_env env j in
   pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -109,7 +110,8 @@ let explain_elim_arity env ind sorts c pj okinds =
     str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++
   fnl () ++ msg
 
-let explain_case_not_inductive env cj =
+let explain_case_not_inductive env sigma cj =
+  let cj = j_nf_evar sigma cj in
   let env = make_all_name_different env in
   let pc = pr_lconstr_env env cj.uj_val in
   let pct = pr_lconstr_env env cj.uj_type in
@@ -121,7 +123,8 @@ let explain_case_not_inductive env cj =
 	  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
 	  str "which is not a (co-)inductive type."
 
-let explain_number_branches env cj expn =
+let explain_number_branches env sigma cj expn =
+  let cj = j_nf_evar sigma cj in
   let env = make_all_name_different env in
   let pc = pr_lconstr_env env cj.uj_val in
   let pct = pr_lconstr_env env cj.uj_type in
@@ -129,11 +132,13 @@ let explain_number_branches env cj expn =
   str "of type" ++ brk(1,1) ++ pct ++ spc () ++
   str "expects " ++  int expn ++ str " branches."
 
-let explain_ill_formed_branch env c i actty expty =
+let explain_ill_formed_branch env sigma c i actty expty =
+  let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
+  let c = nf_evar sigma c in
   let env = make_all_name_different env in
   let pc = pr_lconstr_env env c in
-  let pa = pr_lconstr_env env actty in
-  let pe = pr_lconstr_env env expty in
+  let pa = pr_lconstr_env env (simp actty) in
+  let pe = pr_lconstr_env env (simp expty) in
   str "In pattern-matching on term" ++ brk(1,1) ++ pc ++
   spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++
   brk(1,1) ++ pa ++ spc () ++
@@ -148,7 +153,9 @@ let explain_generalization env (name,var) j =
   str "it has type" ++ spc () ++ pt ++
   spc () ++ str "which should be Set, Prop or Type."
 
-let explain_actual_type env j pt =
+let explain_actual_type env sigma j pt =
+  let j = j_nf_evar sigma j in
+  let pt = nf_evar sigma pt in
   let pe = pr_ne_context_of (str "In environment") env in
   let (pc,pct) = pr_ljudge_env env j in
   let pt = pr_lconstr_env env pt in
@@ -157,7 +164,11 @@ let explain_actual_type env j pt =
   str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
   str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "."
 
-let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl =
+let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
+  let randl = jv_nf_betaiotaevar sigma randl in
+  let exptyp = nf_evar sigma exptyp in
+  let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
+  let rator = j_nf_evar sigma rator in
   let env = make_all_name_different env in
   let nargs = Array.length randl in
 (*  let pe = pr_ne_context_of (str "in environment") env in*)
@@ -179,7 +190,9 @@ let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl =
   str "which should be coercible to" ++ brk(1,1) ++
   pr_lconstr_env env exptyp ++ str "."
 
-let explain_cant_apply_not_functional env rator randl =
+let explain_cant_apply_not_functional env sigma rator randl =
+  let randl = jv_nf_evar sigma randl in
+  let rator = j_nf_evar sigma rator in
   let env = make_all_name_different env in
   let nargs = Array.length randl in
 (*  let pe = pr_ne_context_of (str "in environment") env in*)
@@ -198,13 +211,16 @@ let explain_cant_apply_not_functional env rator randl =
   str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++
   str " " ++ v 0 appl
 
-let explain_unexpected_type env actual_type expected_type =
+let explain_unexpected_type env sigma actual_type expected_type =
+  let actual_type = nf_evar sigma actual_type in
+  let expected_type = nf_evar sigma expected_type in
   let pract = pr_lconstr_env env actual_type in
   let prexp = pr_lconstr_env env expected_type in
   str "Found type" ++ spc () ++ pract ++ spc () ++
   str "where" ++ spc () ++ prexp ++ str " was expected."
 
-let explain_not_product env c =
+let explain_not_product env sigma c =
+  let c = nf_evar sigma c in
   let pr = pr_lconstr_env env c in
   str "The type of this term is a product" ++ spc () ++
   str "while it is expected to be" ++
@@ -293,7 +309,9 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
 	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
     with _ -> mt ())
 
-let explain_ill_typed_rec_body env i names vdefj vargs =
+let explain_ill_typed_rec_body env sigma i names vdefj vargs =
+  let vdefj = jv_nf_evar sigma vdefj in
+  let vargs = Array.map (nf_evar sigma) vargs in
   let env = make_all_name_different env in
   let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in
   let pv = pr_lconstr_env env vargs.(i) in
@@ -303,12 +321,14 @@ let explain_ill_typed_rec_body env i names vdefj vargs =
   str "has type" ++ spc () ++ pvdt ++ spc () ++
   str "while it should be" ++ spc () ++ pv ++ str "."
 
-let explain_cant_find_case_type env c =
+let explain_cant_find_case_type env sigma c =
+  let c = nf_evar sigma c in
   let env = make_all_name_different env in
   let pe = pr_lconstr_env env c in
   str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "."
 
-let explain_occur_check env ev rhs =
+let explain_occur_check env sigma ev rhs =
+  let rhs = nf_evar sigma rhs in
   let env = make_all_name_different env in
   let id = Evd.string_of_existential ev in
   let pt = pr_lconstr_env env rhs in
@@ -352,7 +372,8 @@ let explain_hole_kind env evi = function
   | MatchingVar _ ->
       assert false
 
-let explain_not_clean env ev t k =
+let explain_not_clean env sigma ev t k =
+  let t = nf_evar sigma t in
   let env = make_all_name_different env in
   let id = Evd.string_of_existential ev in
   let var = pr_lconstr_env env t in
@@ -399,13 +420,15 @@ let explain_wrong_case_info env ind ci =
     str "was given to a pattern-matching expression on the inductive type" ++
     spc () ++ pc ++ str "."
 
-let explain_cannot_unify env m n =
+let explain_cannot_unify env sigma m n =
+  let m = nf_evar sigma m in
+  let n = nf_evar sigma n in
   let pm = pr_lconstr_env env m in
   let pn = pr_lconstr_env env n in
   str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
   str "with" ++ brk(1,1) ++ pn ++ str "."
 
-let explain_cannot_unify_local env m n subn =
+let explain_cannot_unify_local env sigma m n subn =
   let pm = pr_lconstr_env env m in
   let pn = pr_lconstr_env env n in
   let psubn = pr_lconstr_env env subn in
@@ -447,7 +470,7 @@ let explain_non_linear_unification env m t =
   strbrk " which would require to abstract twice on " ++
   pr_lconstr_env env t ++ str "."
 
-let explain_type_error env err =
+let explain_type_error env sigma err =
   let env = make_all_name_different env in
   match err with
   | UnboundRel n ->
@@ -455,7 +478,7 @@ let explain_type_error env err =
   | UnboundVar v ->
       explain_unbound_var env v
   | NotAType j ->
-      explain_not_type env j
+      explain_not_type env sigma j
   | BadAssumption c ->
       explain_bad_assumption env c
   | ReferenceVariables id ->
@@ -463,38 +486,39 @@ let explain_type_error env err =
   | ElimArity (ind, aritylst, c, pj, okinds) ->
       explain_elim_arity env ind aritylst c pj okinds
   | CaseNotInductive cj ->
-      explain_case_not_inductive env cj
+      explain_case_not_inductive env sigma cj
   | NumberBranches (cj, n) ->
-      explain_number_branches env cj n
+      explain_number_branches env sigma cj n
   | IllFormedBranch (c, i, actty, expty) ->
-      explain_ill_formed_branch env c i actty expty
+      explain_ill_formed_branch env sigma c i actty expty
   | Generalization (nvar, c) ->
       explain_generalization env nvar c
   | ActualType (j, pt) ->
-      explain_actual_type env j pt
+      explain_actual_type env sigma j pt
   | CantApplyBadType (t, rator, randl) ->
-      explain_cant_apply_bad_type env t rator randl
+      explain_cant_apply_bad_type env sigma t rator randl
   | CantApplyNonFunctional (rator, randl) ->
-      explain_cant_apply_not_functional env rator randl
+      explain_cant_apply_not_functional env sigma rator randl
   | IllFormedRecBody (err, lna, i, fixenv, vdefj) ->
       explain_ill_formed_rec_body env err lna i fixenv vdefj
   | IllTypedRecBody (i, lna, vdefj, vargs) ->
-     explain_ill_typed_rec_body env i lna vdefj vargs
+     explain_ill_typed_rec_body env sigma i lna vdefj vargs
   | WrongCaseInfo (ind,ci) ->
       explain_wrong_case_info env ind ci
 
-let explain_pretype_error env err =
+let explain_pretype_error env sigma err =
+  let env = env_nf_evar sigma env in
   let env = make_all_name_different env in
   match err with
-  | CantFindCaseType c -> explain_cant_find_case_type env c
-  | OccurCheck (n,c) -> explain_occur_check env n c
-  | NotClean (n,c,k) -> explain_not_clean env n c k
+  | CantFindCaseType c -> explain_cant_find_case_type env sigma c
+  | OccurCheck (n,c) -> explain_occur_check env sigma n c
+  | NotClean (n,c,k) -> explain_not_clean env sigma n c k
   | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp
   | VarNotFound id -> explain_var_not_found env id
-  | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect
-  | NotProduct c -> explain_not_product env c
-  | CannotUnify (m,n) -> explain_cannot_unify env m n
-  | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn
+  | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect
+  | NotProduct c -> explain_not_product env sigma c
+  | CannotUnify (m,n) -> explain_cannot_unify env sigma m n
+  | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
   | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
   | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
@@ -502,6 +526,7 @@ let explain_pretype_error env err =
       explain_cannot_find_well_typed_abstraction env p l
   | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
   | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
+  | TypingError t -> explain_type_error env sigma t
 
 (* Typeclass errors *)
 
@@ -809,7 +834,7 @@ let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,c,(env',e)) ->
       str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
       spc () ++ str "is not well typed." ++ fnl () ++
-      explain_type_error env' e
+      explain_type_error env' Evd.empty e
 
 let explain_ltac_call_trace (nrep,last,trace,loc) =
   let calls =
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index dd8a7d663..119765aec 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -19,9 +19,9 @@ open Logic
 
 (** This module provides functions to explain the type errors. *)
 
-val explain_type_error : env -> type_error -> std_ppcmds
+val explain_type_error : env -> Evd.evar_map -> type_error -> std_ppcmds
 
-val explain_pretype_error : env -> pretype_error -> std_ppcmds
+val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> std_ppcmds
 
 val explain_inductive_error : inductive_error -> std_ppcmds
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fe676b3b1..78235f458 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1064,8 +1064,8 @@ let vernac_check_may_eval redexp glopt rc =
     try
       Evarutil.check_evars env sigma sigma' c;
       Typeops.typing env c
-    with P.PretypeError (_,P.UnsolvableImplicit _)
-      | Compat.Loc.Exc_located (_,P.PretypeError (_,P.UnsolvableImplicit _)) ->
+    with P.PretypeError (_,_,P.UnsolvableImplicit _)
+      | Compat.Loc.Exc_located (_,P.PretypeError (_,_,P.UnsolvableImplicit _)) ->
       Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) in
   match redexp with
     | None ->