Bring back the nice printing of automatically generated theorems

4 files changed, 34 insertions, 13 deletions

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 87ea41f..5e984a4 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -84,19 +84,19 @@ let interp_conseq_uf (prem, concl) =
 let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) =
 
   let t_i' = make_t_i rt in
-  let ce5 = Structures.mkConst t_i' in
+  let ce5 = Structures.mkUConst t_i' in
   let ct_i = Term.mkConst (declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition)) in
 
   let t_func' = make_t_func ro ct_i in
-  let ce6 = Structures.mkConst t_func' in
+  let ce6 = Structures.mkUConst t_func' in
   let ct_func = Term.mkConst (declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition)) in
 
   let t_atom' = Atom.interp_tbl ra in
-  let ce1 = Structures.mkConst t_atom' in
+  let ce1 = Structures.mkUConst t_atom' in
   let ct_atom = Term.mkConst (declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition)) in
 
   let t_form' = snd (Form.interp_tbl rf) in
-  let ce2 = Structures.mkConst t_form' in
+  let ce2 = Structures.mkUConst t_form' in
   let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
 
   let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl false in
@@ -112,14 +112,14 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
     let i = ref (l-1) in
     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
     mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
-  let ce3 = Structures.mkConst roots in
+  let ce3 = Structures.mkUConst roots in
   let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
-  let ce3' = Structures.mkConst used_roots in
+  let ce3' = Structures.mkUConst used_roots in
   let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
 
   let certif =
     mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
-  let ce4 = Structures.mkConst certif in
+  let ce4 = Structures.mkUConst certif in
   let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
 
   ()
@@ -180,7 +180,7 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
 	vm_cast_true
 	  (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))) in
 
-  let ce = Structures.mkConst theorem_proof in
+  let ce = Structures.mkTConst theorem_proof theorem_concl in
   let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
   ()
 
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
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
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 20b5463..523bd1d 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -200,14 +200,14 @@ let parse_certif dimacs trace fdimacs ftrace =
   SmtTrace.clear ();
   let _,first,last,reloc = import_cnf fdimacs in
   let d = make_roots first last in
-  let ce1 = Structures.mkConst d in
+  let ce1 = Structures.mkUConst d in
   let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl false in
   let certif = 
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in 
-  let ce2 = Structures.mkConst certif in
+  let ce2 = Structures.mkUConst certif in
   let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in
   ()
 
@@ -240,7 +240,7 @@ let theorem name fdimacs ftrace =
 		  vm_cast_true 
 		    (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]);
                   Term.mkRel 1(*v*)|]))) in
-  let ce = Structures.mkConst theorem_proof in
+  let ce = Structures.mkTConst theorem_proof theorem_type in
   let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
   ()