snapshot

[helm.git] / helm / ocaml / cic_notation / doc / samples.ma

diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma
index f0a75667c18fea4c86ac3d701cfcdead72100986..abd8b7866685aeeb4df42298a916320791def675 100644 (file)
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -35,8 +35,8 @@ print 1 + 2.
 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 render cic:/Coq/Arith/Plus/plus_comm.con.
 
-notation \[ \TERM a + \TERM b \] for 'plus \TERM a \TERM b.
-notation \[ \TERM a * \TERM b \] for 'mult \TERM a \TERM b.
+notation \[ \TERM a + \TERM b \] left associative with precedence 50 for 'plus \TERM a \TERM b.
+notation \[ \TERM a * \TERM b \] left associative with precedence 60 for 'mult \TERM a \TERM b.
 interpretation 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
 interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.