From e781edb69ae6c9e9d5c52646716b60332f98ff59 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 3 Jul 2007 07:05:12 +0000 Subject: Compatibilité des noms longs de Bool déplacés dans Datatypes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9936 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 1bd56a1ee..5cb4bcd5a 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -691,3 +691,11 @@ Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b). Proof. destruct b; intuition. Qed. + +(* Compatibility *) + +Notation andb := Datatypes.andb (only parsing). +Notation orb := Datatypes.orb (only parsing). +Notation implb := Datatypes.implb (only parsing). +Notation xorb := Datatypes.xorb (only parsing). +Notation negb := Datatypes.negb (only parsing). -- cgit v1.2.3