* added group box (?)

[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 f8620ececd5867585f3ba022126a33fabdb58cd2..493db5958912e08f2a41dc78e591cb9fe379fe48 100644 (file)
--- a/helm/ocaml/cic_notation/doc/samples.ma
+++ b/helm/ocaml/cic_notation/doc/samples.ma
@@ -54,7 +54,7 @@ interpretation 'mult x y = (cic:/Coq/Init/Peano/mult.con x y).
 render cic:/Coq/Arith/Mult/mult_plus_distr_r.con.
 
 notation
-  "'if' a 'then' b 'else' c"
+  "hvbox ('if' a 'then' break b break 'else' break c)"
 for
   @{ 'ifthenelse $a $b $c }.
 print if even then \forall x:nat.x else bump x.