diff options
Diffstat (limited to 'contrib/omega/coq_omega.ml')
| -rw-r--r-- | contrib/omega/coq_omega.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index da0817d1..be9ea5ae 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id: coq_omega.ml 8934 2006-06-09 14:30:12Z herbelin $ *) +(* $Id: coq_omega.ml 9963 2007-07-09 14:02:20Z letouzey $ *) open Util open Pp @@ -302,6 +302,7 @@ let coq_eq_ind_r = lazy (constant "eq_ind_r") let coq_dec_or = lazy (constant "dec_or") let coq_dec_and = lazy (constant "dec_and") let coq_dec_imp = lazy (constant "dec_imp") +let coq_dec_iff = lazy (constant "dec_iff") let coq_dec_not = lazy (constant "dec_not") let coq_dec_False = lazy (constant "dec_False") let coq_dec_not_not = lazy (constant "dec_not_not") @@ -312,6 +313,7 @@ let coq_not_and = lazy (constant "not_and") let coq_not_imp = lazy (constant "not_imp") let coq_not_not = lazy (constant "not_not") let coq_imp_simp = lazy (constant "imp_simp") +let coq_iff = lazy (constant "iff") (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) @@ -388,6 +390,8 @@ let destructurate_prop t = | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args) | _, [_;_] when c = build_coq_and () -> Kapp (And,args) | _, [_;_] when c = build_coq_or () -> Kapp (Or,args) + | _, [t1;t2] when c = Lazy.force coq_iff -> + Kapp (And,[mkArrow t1 t2;mkArrow t2 t1]) | _, [_] when c = build_coq_not () -> Kapp (Not,args) | _, [] when c = build_coq_False () -> Kapp (False,args) | _, [] when c = build_coq_True () -> Kapp (True,args) |