diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-30 22:08:11 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-30 22:08:11 +0200 |
| commit | 5a1b0fdd5bab9b40c10d71c09fdb58725e7373bc (patch) | |
| tree | 48a05ea11844e7a1d920900b7ad5e95af84f7d03 /src/zchaff/zchaff.ml | |
| parent | 1aa3a9cb2171de7a68d00fb4c30b81c8d2689979 (diff) | |
| download | smtcoq-5a1b0fdd5bab9b40c10d71c09fdb58725e7373bc.tar.gz smtcoq-5a1b0fdd5bab9b40c10d71c09fdb58725e7373bc.zip | |
Print warnings when checking proofs with holes
Diffstat (limited to 'src/zchaff/zchaff.ml')
| -rw-r--r-- | src/zchaff/zchaff.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 523bd1d..74ae918 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -204,7 +204,7 @@ let parse_certif dimacs trace fdimacs ftrace = 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 (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let ce2 = Structures.mkUConst certif in @@ -223,7 +223,7 @@ let theorem name fdimacs ftrace = 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 + SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in @@ -252,7 +252,7 @@ let checker fdimacs ftrace = 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 + SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in @@ -351,7 +351,7 @@ let build_body reify_atom reify_form l b (max_id, confl) = let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in let (tres,_,_) = - SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl false in + SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let vtvar = Term.mkRel 3 in @@ -372,7 +372,7 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) = let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in let (tres,_,_) = - SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl false in + SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let vtvar = Term.mkRel 3 in |