From 47d1e4d9d09dee1fccce3e2d7b1c7330440bd318 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Sep 2001 13:07:17 +0000
Subject: Suppression des library roots, on teste si un nom est absolu
 autrement

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

(limited to 'toplevel/errors.ml')

diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 11e7c38ccd..cf48f0764c 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -81,6 +81,9 @@ let rec explain_exn_default = function
 	       'sTR "The reference"; 'sPC; Nametab.pr_qualid q;
 	       'sPC ; 'sTR "was not found"; 
 	       'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
+  | Nametab.GlobalizationConstantError q ->
+      hOV 0 [< 'sTR "Error:"; 'sPC;
+	       'sTR "No constant of this name:"; 'sPC; Nametab.pr_qualid q >]
   | Tacmach.FailError i ->
       hOV 0 [< 'sTR "Error: Fail tactic always fails (level "; 
 	       'iNT i; 'sTR")." >]
-- 
cgit v1.2.3