multiple bindings inside OPT supported

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

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index c068491a38898c07e5c7fc1f89c263f9d2b688ba..a8e2c45b0c6231901e2ce4fe131146609ad7cfd8 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -41,7 +41,12 @@ let _ =
       CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
         (P.Layout (P.Box (P.H,
           [ P.Literal (`Symbol "+");
-            P.Magic (P.Opt (P.Variable (P.TermVar "ugo"))) ]
+            P.Magic (P.Opt (P.Layout (P.Box (P.H,
+              [ P.Variable (P.TermVar "ugo");
+                P.Literal (`Symbol "+");
+                P.Variable (P.TermVar "pino")
+              ]))));
+          ]
 (*           [ P.Variable (P.TermVar "a");
             P.Literal (`Symbol "+");
             P.Variable (P.TermVar "b");
@@ -52,10 +57,12 @@ let _ =
           prerr_endline "reducing rule" ;
           prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env));
 (*           match env with
-          [(x, (_, P.OptValue v))] ->
+          [(_, (_, P.OptValue v))] ->
               begin
                 match v with
-                Some _ -> Printf.printf "Ugo c'e'? %s\n" x; flush stdout
+                | Some x ->
+                    printf "Ugo c'e'? %s\n" (CicNotationParser.pp_value x);
+                    flush stdout
                 | None  -> prerr_endline "nooooo"
               end
            | _ -> assert false *)