From 71d22a0cfa99a3c28e59c97e2d3ae68b08c4c47a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 3 Sep 2003 07:17:04 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4297 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/translate.txt | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'dev')

diff --git a/dev/translate.txt b/dev/translate.txt
index 1db8e6212a..f74f8fc8d5 100644
--- a/dev/translate.txt
+++ b/dev/translate.txt
@@ -34,6 +34,28 @@ II) Notations
   Grammar (on constr) and Syntax are no longer supported. Replace them by
 Notation before translation.
 
+  Precedence levels are now from 0 to 250. Typical level are:
+
+  /\ : 60
+  \/ : 70
+  <-> : 80
+  ~ : 50
+  =, <=, >=, <> : 50
+  +, - : 40
+  *, / : 30
+
+  The new scale can induce incompatibilities. To set the level an
+operator should have after translation, use the V8only modifier of
+Infix or Notation in the v7 file, as e.g.:
+
+   Infix 6 "<=" le  V8only 50.
+   Notation "( x , y )" := (pair ? ? x y)  V8only "x , y" (at level 0).
+   Infix 3 "*" mult : nat_scope  V8only (left associativity).
+
+  The default for precedence is to multiply the level by 10. Notice
+that you can change not only the precedence but also the
+associativity and the syntax itself.
+
 III) Main examples for new syntax
      ----------------------------
 
-- 
cgit v1.2.3