From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 14 Feb 2019 20:09:40 +0100 Subject: V8.7 (#36) Port SMTCoq to Coq-8.7 --- src/verit/veritSyntax.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'src/verit/veritSyntax.ml') diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index e209fd2..6b26f65 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -193,18 +193,18 @@ let mkDistinctElim old value = (* Clause difference (wrt to their sets of literals) *) -let clause_diff c1 c2 = - let r = - List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1 - in - Format.eprintf "["; - List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1; - Format.eprintf "] -- ["; - List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2; - Format.eprintf "] ==\n ["; - List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r; - Format.eprintf "] @."; - r +(* let clause_diff c1 c2 = + * let r = + * List.filter (fun t1 -> not (List.exists (SmtAtom.Form.equal t1) c2)) c1 + * in + * Format.eprintf "["; + * List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c1; + * Format.eprintf "] -- ["; + * List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) c2; + * Format.eprintf "] ==\n ["; + * List.iter (Format.eprintf " %a ,\n" SmtAtom.(Form.to_smt Atom.to_smt)) r; + * Format.eprintf "] @."; + * r *) @@ -234,7 +234,7 @@ let rec fins_lemma ids_params = Other (Forall_inst (lemma, _)) -> lemma | _ -> fins_lemma t -let rec find_remove_lemma lemma ids_params = +let find_remove_lemma lemma ids_params = let eq_lemma h = eq_clause lemma (get_clause h) in list_find_remove eq_lemma ids_params @@ -250,7 +250,7 @@ let rec merge ids_params = let to_add = ref [] -let rec mk_clause (id,typ,value,ids_params) = +let mk_clause (id,typ,value,ids_params) = let kind = match typ with (* Roots *) -- cgit