X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=681dfd5e50b83b0369445b7e75280ad35620e38f;hb=cb408b9ea336cd8efb990f7a1c88b566ccf0bd2e;hp=6bc494cdc5801be74a740972c16abf665dd60c9d;hpb=ec54d490477ece51c19d79750dda9805ffda663c;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 6bc494cdc..681dfd5e5 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -144,7 +144,7 @@ let extract_term_production pattern =
         [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
         @ aux p1
     | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-    | Break -> []
+(*     | Break -> [] *)
     | Box (_, pl) -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
@@ -323,7 +323,11 @@ EXTEND
           return_term loc (Layout (Box (H, p)))
       | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
           return_term loc (Layout (Box (V, p)))
-      | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
+      | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box (HV, p)))
+      | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box (HOV, p)))
+(*       | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *)
       | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
           return_term loc (CicNotationUtil.boxify p)
       | p = SELF; SYMBOL "\\AS"; id = IDENT ->