X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Fdoc%2Fsamples.ma;h=ff6380151876bf82ecc32778e96afccd30e57f2a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=803d624c04d0f7a7009fd9fea5520d93988e4fe3;hpb=34113d572c334c351ba66f4b05db503eed4d48f2;p=helm.git

diff --git a/helm/ocaml/cic_notation/doc/samples.ma b/helm/ocaml/cic_notation/doc/samples.ma
index 803d624c0..ff6380151 100644
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -114,7 +114,11 @@ interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 
 notation \[ \TERM a \OVER \TERM b : \TERM c \SQRT \TERM d \] for 'megacoso \TERM a \TERM b \TERM c \TERM d.
-interpretation 'megacoso x y z w = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) (cic:/Coq/Init/Peano/plus.con x y) (cic:/Coq/Init/Peano/plus.con z w)).
+interpretation "megacoso" 'megacoso x y z w =
+  (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)
+    cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
+    (cic:/Coq/Init/Peano/plus.con x y)
+    (cic:/Coq/Init/Peano/plus.con z w)).
 render cic:/Coq/Arith/Plus/plus_comm.con.
 
 # full samples