diff options
| author | notin | 2006-07-18 11:58:04 +0000 |
|---|---|---|
| committer | notin | 2006-07-18 11:58:04 +0000 |
| commit | ccf73b95b086d69fa2706438675c989e6a055921 (patch) | |
| tree | bc342a5ee7a9de4c61fce88997929b572295c3aa /contrib/xml/xmlcommand.ml | |
| parent | 92ec54ec58be0c5c9e7242bb2b55aa1ce2e47cef (diff) | |
Correction bug #1192
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9055 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |