diff options
| author | Brian Campbell | 2019-03-01 10:39:37 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-01 10:39:37 +0000 |
| commit | dfb2ca35204870809730a0feb0ba98c1f45f57ac (patch) | |
| tree | 6b5302b57619c479b72793999cf440a069191041 /src | |
| parent | 7503075ef8e9a3698b7bd9c8033ae36a2d0776b9 (diff) | |
Coq: make iff `iff`
Also drop unused implication function
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 11 |
1 files changed, 2 insertions, 9 deletions
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 = |