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

1 files changed, 11 insertions, 0 deletions

diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index 7e3005962..c9151d829 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -491,6 +491,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}
 
 \begin{minipage}{6in}