aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-17 16:42:37 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-17 16:42:37 +0000
commit5276072c26582cac0ce2f0582824959dc12dad15 (patch)
treefa0e01f767104b4d81538137e83f9cd15caee0f4 /pretyping
parentbc69d8fe0d3585036b1de6d4b43ad80fe49af028 (diff)
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
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions