aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml/xmlcommand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
-rw-r--r--contrib/xml/xmlcommand.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index a653b1c04..815841673 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -726,8 +726,7 @@ let print sp fn =
let hyps = string_list_of_named_context_list hyps in
sp,Inductive,
print_mutual_inductive packs [] hyps env inner_types
- | T.ConstructRef _
- | T.EvarRef _ ->
+ | T.ConstructRef _ ->
Util.anomaly ("print: this should not happen")
in
Xml.pp pp_cmds fn ;