Bring back the nice printing of automatically generated theorems

1 files changed, 15 insertions, 1 deletions

diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 74c484a..26a8cc1 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -68,7 +68,7 @@ type names_id_t = Names.Id.t
 
 let dummy_loc = Loc.ghost
 
-let mkConst c =
+let mkUConst c =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let evd, ty = Typing.type_of env evd c in
@@ -82,6 +82,20 @@ let mkConst c =
     const_entry_opaque      = false;
     const_entry_inline_code = false }
 
+let mkTConst c ty =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, _ = Typing.type_of env evd c in
+  { const_entry_body        = Future.from_val ((c, Univ.ContextSet.empty),
+                                               Safe_typing.empty_private_constants);
+    const_entry_secctx      = None;
+    const_entry_feedback    = None;
+    const_entry_type        = Some ty;
+    const_entry_polymorphic = false;
+    const_entry_universes   = snd (Evd.universe_context evd);
+    const_entry_opaque      = false;
+    const_entry_inline_code = false }
+
 let error = Errors.error
 
 let coqtype = Future.from_val Term.mkSet