aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/xmlcommand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
-rw-r--r--plugins/xml/xmlcommand.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index a34d4a682..ddc4725c3 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -229,8 +229,7 @@ let mk_constant_obj id bo ty variables hyps =
Acic.Constant (Names.Id.to_string id,None,ty,params)
| Some c ->
Acic.Constant
- (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)),
- ty,params)
+ (Names.Id.to_string id, Some (Unshare.unshare c), ty,params)
;;
let mk_inductive_obj sp mib packs variables nparams hyps finite =