From ccf73b95b086d69fa2706438675c989e6a055921 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 18 Jul 2006 11:58:04 +0000
Subject: Correction bug #1192

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9055 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index b6b1c7b68a..4f00a9edb5 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -531,7 +531,7 @@ let print internal glob_ref kind xml_library_root =
             D.mind_finite=finite} = mib in
           Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
     | Ln.ConstructRef _ ->
-       Util.anomaly ("print: this should not happen")
+       Util.error ("a single constructor cannot be printed in XML")
   in
   let fn = filename_of_path xml_library_root tag in
   let uri = Cic2acic.uri_of_kernel_name tag in
-- 
cgit v1.2.3