From 2e43dde0f53e8aa1e0afc9d0c214825678aec481 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 8 Oct 2009 17:45:32 +0000
Subject: Fixed clash names in Relations (see bug report #2152) and make names
 in Relation_Operators.v and Operators_Properties.v more uniform in general.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/naming-conventions.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index 7e30059629..c9151d8295 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -490,6 +490,17 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}.
 
   Remark: Use \name{Drel\_rel'\_weak} for a strict inclusion ??
 
+%======================================================================
+\section{Relations between properties}
+
+\itemrule{Equivalence of properties \texttt{P} and \texttt{Q}}{P\_Q\_iff}
+{forall x1 .. xn, P <-> Q}
+
+  Remark: Alternatively use \name{P\_iff\_Q} if it is too difficult to
+  recover what pertains to \texttt{P} and what pertains to \texttt{Q}
+  in their concatenation (as e.g. in
+  \texttt{Godel\_Dummett\_iff\_right\_distr\_implication\_over\_disjunction}).
+
 %======================================================================
 \section{Arithmetical conventions}
 
-- 
cgit v1.2.3