diff options
author | ckeller <ckeller@users.noreply.github.com> | 2019-02-14 20:09:40 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-14 20:09:40 +0100 |
commit | ec41af7ac01cef7c30785e6dd704381f31e7c2d3 (patch) | |
tree | 13d51483c50d7b5a668d90b8b67a8b99ef0fbe56 /src/verit/veritSyntax.ml | |
parent | ba22fad2fb46962eef5f30d976e9eaeb587023a0 (diff) | |
download | smtcoq-ec41af7ac01cef7c30785e6dd704381f31e7c2d3.tar.gz smtcoq-ec41af7ac01cef7c30785e6dd704381f31e7c2d3.zip |
V8.7 (#36)
Port SMTCoq to Coq-8.7
Diffstat (limited to 'src/verit/veritSyntax.ml')
-rw-r--r-- | src/verit/veritSyntax.ml | 28 |
1 files changed, 14 insertions, 14 deletions
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 *) |