diff options
author | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /contrib/omega | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'contrib/omega')
-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) |