aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml')
-rw-r--r--plugins/xml/acic2Xml.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 9d3a10dba..73f113d6a 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -26,7 +26,7 @@ let rec find_last_id =
| _::tl -> find_last_id tl
;;
-let export_existential = string_of_int
+let export_existential ev = string_of_int (Evar.repr ev)
let print_term ids_to_inner_sorts =
let rec aux =