]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed typo in helpers for generating hv and hov boxes
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 26 Jul 2005 14:58:55 +0000 (14:58 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 26 Jul 2005 14:58:55 +0000 (14:58 +0000)
helm/ocaml/cic_notation/box.ml

index 3c079d3162701d72397abad40d84a8d8fd09843d..241214f9ce883aa993deef1695458b2c1df3d3dc 100644 (file)
@@ -111,8 +111,8 @@ let document_of_box ~obj2xml pres =
 
 let b_h a b = H(a,b)
 let b_v a b = V(a,b)
-let b_hv a b = H(a,b)
-let b_hov a b = V(a,b)
+let b_hv a b = HV(a,b)
+let b_hov a b = HOV(a,b)
 let b_text a b = Text(a,b)
 let b_object b = Object ([],b)
 let b_indent = indent