From fa7da17cde94bdeae47cf2bd36b92469d8674cd1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 9 Aug 2017 21:53:06 +0200 Subject: [PATCH] Fix Coq backend Uses a more complete tactic to go from or-separated clause to the negation-implication encoding of clauses used by the coq backend. Also uses a better suffix for temporary clauses than "_or". --- src/backend/coq.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/backend/coq.ml b/src/backend/coq.ml index dfc7e90d..b09ab7d5 100644 --- a/src/backend/coq.ml +++ b/src/backend/coq.ml @@ -32,7 +32,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom end) let name c = c.S.St.name - let name_tmp c = c.S.St.name ^ "_or" + let name_tmp c = c.S.St.name ^ "_tmp" let pp_atom fmt a = if a == S.St.(a.var.pa) then @@ -65,8 +65,8 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom m let clausify fmt clause = - Format.fprintf fmt "assert (%s: %a).@\nintros; try destruct %s; auto. clear %s.@\n" - (name clause) pp_clause clause (name_tmp clause) (name_tmp clause) + Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n" + (name clause) pp_clause clause (name_tmp clause) let elim_duplicate fmt goal hyp _ = (** Printing info comment in coq *)