ocaml 3.09 transition

[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 803d624c04d0f7a7009fd9fea5520d93988e4fe3..ff6380151876bf82ecc32778e96afccd30e57f2a 100644 (file)
--- 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