diff options
Diffstat (limited to 'src/trace/smtCommands.ml')
-rw-r--r-- | src/trace/smtCommands.ml | 16 |
1 files changed, 8 insertions, 8 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 () |