aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ide_slave.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ide_slave.ml')
-rw-r--r--ide/ide_slave.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index e3e1a8890..2065a4546 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -255,7 +255,7 @@ let status force =
let export_coq_object t = {
Interface.coq_object_prefix = t.Search.coq_object_prefix;
Interface.coq_object_qualid = t.Search.coq_object_qualid;
- Interface.coq_object_object = t.Search.coq_object_object
+ Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
}
let pattern_of_string ?env s =