From d21d934c5ef9f47046a705eebd554e63f77b9e30 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 15:23:16 +0000
Subject:  - états fabriqués avec -silent  - compilation theories avec -q  -
 correction but de tclORELSE qui doit maintenant rattraper aussi    TypeError
 et RefinerError

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@249 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/errors.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'toplevel/errors.ml')

diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index ba1f36cd7c..ad4f6f389b 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -52,6 +52,8 @@ let rec explain_exn_default = function
 
   | InductiveError e -> hOV 0 (Himsg.explain_inductive_error e)
 
+  | Logic.RefinerError e -> hOV 0 (Himsg.explain_refiner_error e)
+
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
                else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
-- 
cgit v1.2.3