From 1aa3a9cb2171de7a68d00fb4c30b81c8d2689979 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Sat, 30 Apr 2016 19:54:54 +0200
Subject: Bring back the nice printing of automatically generated theorems

---
 src/versions/native/structures.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/versions/native')

diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 6eb1991..51e14d6 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -45,13 +45,20 @@ type names_id_t = Names.identifier
 
 let dummy_loc = Pp.dummy_loc
 
-let mkConst c =
+let mkUConst c =
   { const_entry_body = c;
     const_entry_type = None;
     const_entry_secctx = None;
     const_entry_opaque = false;
     const_entry_inline_code = false}
 
+let mkTConst c ty =
+  { const_entry_body = c;
+    const_entry_type = Some ty;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
 let error = Errors.error
 
 let coqtype = lazy Term.mkSet
-- 
cgit