From dfb2ca35204870809730a0feb0ba98c1f45f57ac Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 1 Mar 2019 10:39:37 +0000
Subject: Coq: make iff `iff` Also drop unused implication function

---
 src/pretty_print_coq.ml | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 5dfeb7ba..d205e46b 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -350,21 +350,14 @@ match nc1, nc2 with
 | _, NC_aux (NC_true,_) -> nc1
 | _,_ -> nc_and nc1 nc2
 
-let nice_imp nc1 nc2 =
-match nc1, nc2 with
-| NC_aux (NC_true,_), _ -> nc2
-| _, NC_aux (NC_true,_) -> nc2
-| NC_aux (NC_false,l), _ -> NC_aux (NC_true,l)
-| _, NC_aux (NC_false,_) -> nc_not nc1
-| _,_ -> nc_or (nc_not nc1) nc2
-
 let nice_iff nc1 nc2 =
 match nc1, nc2 with
 | NC_aux (NC_true,_), _ -> nc2
 | _, NC_aux (NC_true,_) -> nc1
 | NC_aux (NC_false,_), _ -> nc_not nc2
 | _, NC_aux (NC_false,_) -> nc_not nc1
-| _,_ -> nc_or (nc_and nc1 nc2) (nc_and (nc_not nc1) (nc_not nc2))
+ (* TODO: replace this hacky iff with a proper NC_ constructor *)
+| _,_ -> mk_nc (NC_app (mk_id "iff",[arg_bool nc1; arg_bool nc2]))
 
 (* n_constraint functions are currently just Z3 functions *)
 let doc_nc_fn_prop id =
-- 
cgit v1.2.3