* added group box (?)

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index f4651d6374e0452583be24f117eee5e6794f83aa..472389de3903e0f68edf92aa4b97f4062c700f3e 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -166,6 +166,7 @@ let extract_term_production pattern =
     | Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p
     | Break -> []
     | Box (_, pl) -> List.flatten (List.map aux pl)
+    | Group pl -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
     | Opt p ->
@@ -353,17 +354,17 @@ EXTEND
       | SYMBOL "\\root"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
           return_term loc (Layout (Root (arg, index)))
       | "hbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (CicNotationUtil.boxify p)
+          return_term loc (Layout (Box ((H, false, false), p)))
       | "vbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (CicNotationUtil.boxify p)
+          return_term loc (Layout (Box ((V, false, false), p)))
       | "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (CicNotationUtil.boxify p)
+          return_term loc (Layout (Box ((HV, false, false), p)))
       | "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (CicNotationUtil.boxify p)
+          return_term loc (Layout (Box ((HOV, false, false), p)))
       | "break" -> return_term loc (Layout Break)
 (*       | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
       | LPAREN; p = l1_pattern; RPAREN ->
-          return_term loc (CicNotationUtil.boxify p)
+          return_term loc (CicNotationUtil.group p)
       ]
     | "simple" NONA
       [ i = IDENT -> return_term loc (Variable (TermVar i))