From 5276072c26582cac0ce2f0582824959dc12dad15 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 17 Apr 2008 16:42:37 +0000 Subject: No compatibility notations for andb and co (this restore a correct Print output) The benefit of these "only-parsing" notations in Bool.v were to avoid replacing qualified Bool.andb by Datatypes.andb and so on. But such Bool.xxxx are fairly rare (e.g. none in contribs), and these notations have one serious drawback: with them, Print andb leads to Datatypes.andb instead of the body of andb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10812 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 7 ------- 1 file changed, 7 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index bae2e14ab..2995f0515 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -723,10 +723,3 @@ Proof. 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