Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation

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

9 files changed, 175 insertions, 178 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 225756a99..bf0a99ee3 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -45,20 +45,6 @@ type type_error =
   | IllFormedRecBody of guard_error * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * types array
-  | NotInductive of constr
-  | MLCase of string * constr * constr * constr * constr
-  | CantFindCaseType of constr
-  | OccurCheck of int * constr
-  | NotClean of int * constr
-  | VarNotFound of identifier
-  | UnexpectedType of constr * constr
-  | NotProduct of constr
-  (* Pattern-matching errors *)
-  | BadPattern of constructor * constr
-  | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor_path * int
-  | WrongPredicateArity of constr * constr * constr
-  | NeedsInversion of constr * constr
 
 exception TypeError of path_kind * env * type_error
 
@@ -107,15 +93,4 @@ let error_ill_formed_rec_body k env why lna i vdefs =
 let error_ill_typed_rec_body k env i lna vdefj vargs =
   raise (TypeError (k, env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
-let error_not_inductive k env c =
-  raise (TypeError (k, env, NotInductive c))
-
-let error_ml_case k env mes c ct br brt =
-  raise (TypeError (k, env, MLCase (mes,c,ct,br,brt)))
-
-let error_unexpected_type env actual expected =
-  raise (TypeError (CCI, env, UnexpectedType (actual, expected)))
-
-let error_not_product env c =
-  raise (TypeError (CCI, env, NotProduct c))
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index e7e850c71..c45fac721 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -49,20 +49,6 @@ type type_error =
   | IllFormedRecBody of guard_error * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
       * types array
-  | NotInductive of constr
-  | MLCase of string * constr * constr * constr * constr
-  | CantFindCaseType of constr
-  | OccurCheck of int * constr
-  | NotClean of int * constr
-  | VarNotFound of identifier
-  | UnexpectedType of constr * constr
-  | NotProduct of constr
-  (* Pattern-matching errors *)
-  | BadPattern of constructor * constr
-  | BadConstructor of constructor * inductive
-  | WrongNumargConstructor of constructor_path * int
-  | WrongPredicateArity of constr * constr * constr
-  | NeedsInversion of constr * constr
 
 exception TypeError of path_kind * env * type_error
 
@@ -107,11 +93,3 @@ val error_ill_typed_rec_body  :
   path_kind -> env -> int -> name list -> unsafe_judgment array 
     -> types array -> 'b
 
-val error_not_inductive : path_kind -> env -> constr -> 'a
-
-val error_ml_case : path_kind -> env -> 
-  string -> constr -> constr -> constr -> constr -> 'a
-
-val error_unexpected_type : env -> actual:constr -> expected:constr -> 'a
-
-val error_not_product : env -> constr -> 'a
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3b6acb1ba..c155c4555 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -197,7 +197,7 @@ let real_clean isevars sp args rhs =
       | _ -> map_constr_with_binders succ subs k t
   in
   let body = subs 0 rhs in
-  if not (closed0 body) then error_not_clean CCI empty_env sp body;
+  if not (closed0 body) then error_not_clean empty_env sp body;
   body
 
 let make_evar_instance_with_rel env =
@@ -253,7 +253,7 @@ let keep_rels_and_vars c = match kind_of_term c with
   | _ -> mkImplicit   (* Mettre mkMeta ?? *)
 
 let evar_define isevars (ev,argsv) rhs =
-  if occur_evar ev rhs then error_occur_check CCI empty_env ev rhs;
+  if occur_evar ev rhs then error_occur_check empty_env ev rhs;
   let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
   (* the substitution to invert *)
@@ -449,8 +449,7 @@ let split_tycon loc env isevars = function
 	      isevars := sigma;
 	      Some dom, Some rng
 	    else
-	      Stdpp.raise_with_loc loc
-		(Type_errors.TypeError (CCI,env,Type_errors.NotProduct c))
+	      error_not_product_loc loc env c
 
 let valcon_of_tycon x = x
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ff57b0012..985b7975c 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -3,65 +3,81 @@
 
 open Names
 open Sign
+open Term
 open Environ
 open Type_errors
 open Rawterm
 
-let raise_pretype_error (loc,k,ctx,te) =
-  Stdpp.raise_with_loc loc (TypeError(k,ctx,te))
+type ml_case_error =
+  | MlCaseAbsurd
+  | MlCaseDependent
+
+type pretype_error =
+  (* Old Case *)
+  | MlCase of ml_case_error
+  | CantFindCaseType of constr
+  (* Unification *)
+  | OccurCheck of int * constr
+  | NotClean of int * constr
+  (* Pretyping *)
+  | VarNotFound of identifier
+  | UnexpectedType of constr * constr
+  | NotProduct of constr
+
+exception PretypeError of env * pretype_error
 
-let error_var_not_found_loc loc k s =
-  raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s)
+let raise_pretype_error (loc,ctx,te) =
+  Stdpp.raise_with_loc loc (PretypeError(ctx,te))
+
+let raise_located_type_error (loc,k,ctx,te) =
+  Stdpp.raise_with_loc loc (TypeError(k,ctx,te))
 
 let error_cant_find_case_type_loc loc env expr =
-  raise_pretype_error (loc, CCI, env, CantFindCaseType expr)
+  raise_pretype_error (loc, env, CantFindCaseType expr)
+
+let error_ill_formed_branch_loc loc k env c i actty expty =
+  raise_located_type_error (loc, k, env, IllFormedBranch (c,i,actty,expty))
 
 let error_actual_type_loc loc env c actty expty =
-  raise_pretype_error (loc, CCI, env, ActualType (c,actty,expty))
+  raise_located_type_error (loc, CCI, env, ActualType (c,actty,expty))
 
 let error_cant_apply_not_functional_loc loc env rator randl =
-  raise_pretype_error
+  raise_located_type_error
     (loc,CCI,env, CantApplyNonFunctional (rator,randl))
 
 let error_cant_apply_bad_type_loc loc env t rator randl =
-  raise_pretype_error (loc, CCI, env, CantApplyBadType (t,rator,randl))
+  raise_located_type_error (loc, CCI, env, CantApplyBadType (t,rator,randl))
 
 let error_ill_formed_branch k env c i actty expty =
   raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
 
 let error_number_branches_loc loc k env c ct expn =
-  raise_pretype_error (loc, k, env, NumberBranches (c,ct,expn))
+  raise_located_type_error (loc, k, env, NumberBranches (c,ct,expn))
 
 let error_case_not_inductive_loc loc k env c ct =
-  raise_pretype_error (loc, k, env, CaseNotInductive (c,ct))
+  raise_located_type_error (loc, k, env, CaseNotInductive (c,ct))
 
-(* Pattern-matching errors *)
 
-let error_bad_pattern_loc loc k cstr ind =
-  raise_pretype_error (loc, k, Global.env(), BadPattern (cstr,ind))
+(*s Implicit arguments synthesis errors *)
 
-let error_bad_constructor_loc loc k cstr ind =
-  raise_pretype_error (loc, k, Global.env(), BadConstructor (cstr,ind))
+let error_occur_check env ev c =
+  raise (PretypeError (env, OccurCheck (ev,c)))
 
-let error_wrong_numarg_constructor_loc loc k c n =
-  raise_pretype_error (loc, k, Global.env(), WrongNumargConstructor (c,n))
+let error_not_clean env ev c =
+  raise (PretypeError (env, NotClean (ev,c)))
 
-let error_wrong_predicate_arity_loc loc env c n1 n2 =
-  raise_pretype_error (loc, CCI, env, WrongPredicateArity (c,n1,n2))
+(*s Ml Case errors *)
 
-let error_needs_inversion k env x t =
-  raise (TypeError (k, env, NeedsInversion (x,t)))
+let error_ml_case_loc loc env mes =
+  raise_pretype_error (loc, env, MlCase mes)
 
-let error_ill_formed_branch_loc loc k env c i actty expty =
-  raise_pretype_error (loc, k, env, IllFormedBranch (c,i,actty,expty))
+(*s Pretyping errors *)
 
-(*s Implicit arguments synthesis errors *)
+let error_var_not_found_loc loc s =
+  raise_pretype_error (loc, Global.env() (*bidon*), VarNotFound s)
 
 let error_unexpected_type_loc loc env actty expty =
-  raise_pretype_error (loc, CCI, env, UnexpectedType (actty, expty))
-
-let error_occur_check k env ev c =
-  raise (TypeError (k, env, OccurCheck (ev,c)))
+  raise_pretype_error (loc, env, UnexpectedType (actty, expty))
 
-let error_not_clean k env ev c =
-  raise (TypeError (k, env, NotClean (ev,c)))
+let error_not_product_loc loc env c =
+  raise_pretype_error (loc, env, NotProduct c)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index a48329bd1..ba8c0e4e7 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -13,10 +13,25 @@ open Rawterm
 
 (*s The type of errors raised by the pretyper *)
 
-val error_var_not_found_loc :
-  loc -> path_kind -> identifier -> 'a
-
-val error_cant_find_case_type_loc : 
+type ml_case_error =
+  | MlCaseAbsurd
+  | MlCaseDependent
+
+type pretype_error =
+  (* Old Case *)
+  | MlCase of ml_case_error
+  | CantFindCaseType of constr
+  (* Unification *)
+  | OccurCheck of int * constr
+  | NotClean of int * constr
+  (* Pretyping *)
+  | VarNotFound of identifier
+  | UnexpectedType of constr * constr
+  | NotProduct of constr
+
+exception PretypeError of env * pretype_error
+
+val error_cant_find_case_type_loc :
   loc -> env -> constr -> 'a
 
 val error_ill_formed_branch_loc : 
@@ -38,29 +53,20 @@ val error_number_branches_loc :
 val error_case_not_inductive_loc :
   loc -> path_kind -> env -> constr -> constr -> 'b
 
-(*s Pattern-matching errors *)
-
-val error_bad_pattern_loc : 
-  loc -> path_kind -> constructor -> constr -> 'b
+(*s Implicit arguments synthesis errors *)
 
-val error_bad_constructor_loc : 
-  loc -> path_kind -> constructor -> inductive -> 'b
+val error_occur_check : env -> int -> constr -> 'a
 
-val error_wrong_numarg_constructor_loc : 
-  loc -> path_kind -> constructor_path -> int -> 'b
+val error_not_clean : env -> int -> constr -> 'a
 
-val error_wrong_predicate_arity_loc :
-  loc -> env -> constr -> constr -> constr -> 'b
+(*s Ml Case errors *)
 
-val error_needs_inversion : path_kind -> env -> constr -> constr -> 'a
+val error_ml_case_loc : loc -> env -> ml_case_error -> 'a
 
+(*s Pretyping errors *)
 
-(*s Implicit arguments synthesis errors *)
+val error_var_not_found_loc : loc -> identifier -> 'a
 
 val error_unexpected_type_loc : loc -> env -> constr -> constr -> 'b
 
-val error_occur_check : path_kind -> env -> int -> constr -> 'a
-
-val error_not_clean : path_kind -> env -> int -> constr -> 'a
-
-
+val error_not_product_loc : loc -> env -> constr -> 'a
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ba3e56aea..806a84d66 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -160,7 +160,7 @@ let pretype_id loc env lvar id =
     let typ = lookup_id_type id (named_context env) in
     { uj_val  = mkVar id; uj_type = typ }
   with Not_found ->
-    error_var_not_found_loc loc CCI id
+    error_var_not_found_loc loc id
 
 (*************************************************************************)
 (* Main pretyping function                                               *)
@@ -372,7 +372,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 		      pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
 		    let efjt = nf_ise1 !isevars fj.uj_type in 
 		    let pred = 
-		      Cases.pred_case_ml_onebranch env !isevars isrec indt
+		      Cases.pred_case_ml_onebranch loc env !isevars isrec indt
 			(i,fj.uj_val,efjt) in
 		    if has_undefined_isevars isevars pred then findtype (i+1)
 		    else 
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index f04e99e79..708832d30 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -6,6 +6,7 @@ open Util
 open Ast
 open Indtypes
 open Type_errors
+open Pretype_errors
 open Lexer
 
 let print_loc loc =
@@ -59,8 +60,13 @@ let rec explain_exn_default = function
       hOV 0 [< 'sTR "Error: Universe Inconsistency." >]
   | TypeError(k,ctx,te) -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >]
+  | PretypeError(ctx,te) -> 
+      hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >]
   | InductiveError e -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >]
+  | Cases.PatternMatchingError (env,e) -> 
+      hOV 0
+	[< 'sTR "Error:"; 'sPC; Himsg.explain_pattern_matching_error env e >]
   | Logic.RefinerError e -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_refiner_error e >]
   | Nametab.GlobalizationError q ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4a9c134f9..2abfb6cc1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -10,8 +10,10 @@ open Inductive
 open Indtypes
 open Sign
 open Environ
+open Pretype_errors
 open Type_errors
 open Reduction
+open Cases
 open Logic
 open Pretty
 open Printer
@@ -225,27 +227,14 @@ let explain_not_inductive k ctx c =
   [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
      'sTR "is not an inductive definition" >]
 
-let explain_ml_case k ctx mes c ct br brt =
-  let pc = prterm_env ctx c in
-  let pct = prterm_env ctx ct in
-  let expln =
-    match mes with
-      | "Inductive" -> [< pct; 'sTR "is not an inductive definition">]
-      | "Predicate" -> [< 'sTR "ML case not allowed on a predicate">]
-      | "Absurd" -> [< 'sTR "Ill-formed case expression on an empty type" >]
-      | "Decomp" ->
-          let plf = prterm_env ctx br in
-          let pft = prterm_env ctx brt in
-          [< 'sTR "The branch "; plf; 'wS 1; 'cUT; 'sTR "has type "; pft;
-             'wS 1; 'cUT;
-             'sTR "does not correspond to the inductive definition" >]
-      | "Dependent" ->
-          [< 'sTR "ML case not allowed for a dependent case elimination">]
-      | _ -> [<>]
+let explain_ml_case k ctx mes =
+  let expln = match mes with
+    | MlCaseAbsurd ->
+	[< 'sTR "Unable to infer a predicate for an elimination an empty type">]
+    | MlCaseDependent ->
+        [< 'sTR "Unable to infer a dependent elimination predicate">]
   in
-  hOV 0 [< 'sTR "In ML case expression on "; pc; 'wS 1; 'cUT ;
-           'sTR "of type";  'wS 1; pct; 'wS 1; 'cUT; 
-           'sTR "which is an inductive predicate."; 'fNL; expln >]
+  hOV 0 [< 'sTR "Cannot infer ML Case predicate:"; 'fNL; expln >] 
 
 let explain_cant_find_case_type k ctx c =
   let pe = prterm_env ctx c in
@@ -279,41 +268,6 @@ let explain_var_not_found k ctx id =
      'sPC ; 'sTR "was not found"; 
      'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
 
-(* Pattern-matching errors *)
-let explain_bad_pattern k ctx cstr ty = 
-  let pt = prterm_env ctx ty in
-  let pc = pr_constructor ctx cstr in
-  [< 'sTR "Found the constructor "; pc; 'bRK(1,1); 
-     'sTR "while matching a term of type "; pt; 'bRK(1,1); 
-     'sTR "which is not an inductive type" >]
-
-let explain_bad_constructor k ctx cstr ind =
-  let pi = pr_inductive ctx ind in
-  let pc = pr_constructor ctx cstr in
-  let pt = pr_inductive ctx (inductive_of_constructor cstr) in
-  [< 'sTR "Expecting a constructor in inductive type "; pi; 'bRK(1,1) ;
-     'sTR " but found the constructor " ; pc; 'bRK(1,1) ;
-     'sTR " in inductive type "; pt >]
-
-let explain_wrong_numarg_of_constructor k ctx cstr n =
-  let pc = pr_constructor ctx (cstr,[||]) in
-  [<'sTR "The constructor "; pc;
-    'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">]
-
-let explain_wrong_predicate_arity k ctx pred nondep_arity dep_arity=
-  let pp = prterm_env ctx pred in
-  [<'sTR "The elimination predicate "; 'sPC; pp; 'fNL;
-    'sTR "should be of arity" ; 'sPC;
-    prterm_env ctx nondep_arity ; 'sPC; 'sTR "(for non dependent case) or" ;
-    'sPC; prterm_env ctx dep_arity ; 'sPC; 'sTR "(for dependent case).">]
-
-let explain_needs_inversion k ctx x t =
-  let px = prterm_env ctx x in
-  let pt = prterm_env ctx t in
-  [< 'sTR "Sorry, I need inversion to compile pattern matching of term ";
-     px ; 'sTR " of type: "; pt>]
-
-
 let explain_type_error k ctx = function
   | UnboundRel n -> 
       explain_unbound_rel k ctx n
@@ -343,33 +297,27 @@ let explain_type_error k ctx = function
       explain_ill_formed_rec_body k ctx i lna vdefj vargs
   | IllTypedRecBody (i, lna, vdefj, vargs) -> 
      explain_ill_typed_rec_body k ctx i lna vdefj vargs
+(*
   | NotInductive c ->
       explain_not_inductive k ctx c
-  | MLCase (mes,c,ct,br,brt) ->
-      explain_ml_case k ctx mes c ct br brt
+*)
+let explain_pretype_error ctx = function
+  | MlCase mes ->
+      explain_ml_case CCI ctx mes
   | CantFindCaseType c ->
-      explain_cant_find_case_type k ctx c
+      explain_cant_find_case_type CCI ctx c
   | OccurCheck (n,c) ->
-      explain_occur_check k ctx n c
+      explain_occur_check CCI ctx n c
   | NotClean (n,c) ->
-      explain_not_clean k ctx n c
+      explain_not_clean CCI ctx n c
   | VarNotFound id ->
-      explain_var_not_found k ctx id
+      explain_var_not_found CCI ctx id
   | UnexpectedType (actual,expected) ->
-      explain_unexpected_type k ctx actual expected
+      explain_unexpected_type CCI ctx actual expected
   | NotProduct c ->
-      explain_not_product k ctx c
-  (* Pattern-matching errors *)
-  | BadPattern (c,t) ->
-      explain_bad_pattern k ctx c t
-  | BadConstructor (c,ind) ->
-      explain_bad_constructor k ctx c ind
-  | WrongNumargConstructor (c,n) ->
-      explain_wrong_numarg_of_constructor k ctx c n
-  | WrongPredicateArity (pred,n,dep) ->
-      explain_wrong_predicate_arity k ctx pred n dep
-  | NeedsInversion (x,t) ->
-      explain_needs_inversion k ctx x t
+      explain_not_product CCI ctx c
+
+(* Refiner errors *)
 
 let explain_refiner_bad_type arg ty conclty =
   [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
@@ -422,6 +370,8 @@ let explain_refiner_error = function
   | IntroNeedsProduct -> explain_intro_needs_product ()
   | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
 
+(* Inductive errors *)
+
 let error_non_strictly_positive k env c v  =
   let pc = prterm_env env c in
   let pv = prterm_env env v in
@@ -500,3 +450,63 @@ let explain_inductive_error = function
   | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
   | NotMutualInScheme -> error_not_mutual_in_scheme ()
 
+(* Pattern-matching errors *)
+
+let explain_bad_pattern ctx cstr ty = 
+  let pt = prterm_env ctx ty in
+  let pc = pr_constructor ctx cstr in
+  [< 'sTR "Found the constructor "; pc; 'bRK(1,1); 
+     'sTR "while matching a term of type "; pt; 'bRK(1,1); 
+     'sTR "which is not an inductive type" >]
+
+let explain_bad_constructor ctx cstr ind =
+  let pi = pr_inductive ctx ind in
+  let pc = pr_constructor ctx cstr in
+  let pt = pr_inductive ctx (inductive_of_constructor cstr) in
+  [< 'sTR "Expecting a constructor in inductive type "; pi; 'bRK(1,1) ;
+     'sTR " but found the constructor " ; pc; 'bRK(1,1) ;
+     'sTR " in inductive type "; pt >]
+
+let explain_wrong_numarg_of_constructor ctx cstr n =
+  let pc = pr_constructor ctx (cstr,[||]) in
+  [<'sTR "The constructor "; pc;
+    'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">]
+
+let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity=
+  let pp = prterm_env ctx pred in
+  [<'sTR "The elimination predicate "; 'sPC; pp; 'fNL;
+    'sTR "should be of arity" ; 'sPC;
+    prterm_env ctx nondep_arity ; 'sPC; 'sTR "(for non dependent case) or" ;
+    'sPC; prterm_env ctx dep_arity ; 'sPC; 'sTR "(for dependent case).">]
+
+let explain_needs_inversion ctx x t =
+  let px = prterm_env ctx x in
+  let pt = prterm_env ctx t in
+  [< 'sTR "Sorry, I need inversion to compile pattern matching of term ";
+     px ; 'sTR " of type: "; pt>]
+
+let explain_redundant_clauses env pats =
+  let s = if List.length pats > 1 then "s" else "" in
+  [<'sTR ("Redundant clause for pattern"^s); 'sPC;
+    hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats) >]
+
+let explain_non_exhaustive env pats =
+  let s = if List.length pats > 1 then "s" else "" in
+  [<'sTR ("Non exhaustive pattern-matching: no clause found for pattern"^s);
+    'sPC; hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats) >]
+
+let explain_pattern_matching_error env = function
+  | BadPattern (c,t) -> 
+      explain_bad_pattern env c t
+  | BadConstructor (c,ind) ->
+      explain_bad_constructor env c ind
+  | WrongNumargConstructor (c,n) ->
+      explain_wrong_numarg_of_constructor env c n
+  | WrongPredicateArity (pred,n,dep) ->
+      explain_wrong_predicate_arity env pred n dep
+  | NeedsInversion (x,t) ->
+      explain_needs_inversion env x t
+  | RedundantClause tms ->
+      explain_redundant_clauses env tms
+  | NonExhaustive tms ->
+      explain_non_exhaustive env tms
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index b67922758..57300f5c0 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -7,6 +7,8 @@ open Names
 open Indtypes
 open Environ
 open Type_errors
+open Pretype_errors
+open Cases
 open Logic
 (*i*)
 
@@ -14,6 +16,11 @@ open Logic
 
 val explain_type_error : path_kind -> env -> type_error -> std_ppcmds
 
+val explain_pretype_error : env -> pretype_error -> std_ppcmds
+
 val explain_inductive_error : inductive_error -> std_ppcmds
 
 val explain_refiner_error : refiner_error -> std_ppcmds
+
+val explain_pattern_matching_error :
+  env -> pattern_matching_error -> std_ppcmds