X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2Ftest_parser.ml;h=6cbb0ef2d5d8fd0b7f449331bd3faeed52c1c1d8;hb=078ef847d4a3a2087f2dc404e48bcef76ee4b4d5;hp=a8e2c45b0c6231901e2ce4fe131146609ad7cfd8;hpb=29aacd800408d16b9cb58dd58e603e31aa2ad511;p=helm.git

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index a8e2c45b0..6cbb0ef2d 100644
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -40,33 +40,32 @@ let _ =
     let id =
       CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
         (P.Layout (P.Box (P.H,
-          [ P.Literal (`Symbol "+");
+          [
+            P.Magic
+              (P.List0
+                (P.Layout (P.Box (P.H,
+                  [ P.Literal (`Symbol "|");
+                    P.Variable (P.TermVar "ugo");
+                    P.Magic (P.Opt (P.Layout (P.Box (P.H,
+                      [ P.Literal (`Symbol ",");
+                        P.Variable (P.TermVar "pino")]))));
+                    P.Literal (`Symbol "|");
+                  ])),
+                  Some (`Symbol ";")));
+(*             P.Literal (`Symbol "+");
             P.Magic (P.Opt (P.Layout (P.Box (P.H,
-              [ P.Variable (P.TermVar "ugo");
+              [
+                P.Variable (P.TermVar "ugo");
                 P.Literal (`Symbol "+");
                 P.Variable (P.TermVar "pino")
-              ]))));
-          ]
-(*           [ P.Variable (P.TermVar "a");
+              ])))); *)
+(*           P.Variable (P.TermVar "a");
             P.Literal (`Symbol "+");
-            P.Variable (P.TermVar "b");
-          ] *)
-            )))
+            P.Variable (P.TermVar "b"); *)
+          ])))
         (fun env _ ->
-          begin
           prerr_endline "reducing rule" ;
           prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env));
-(*           match env with
-          [(_, (_, P.OptValue v))] ->
-              begin
-                match v with
-                | Some x ->
-                    printf "Ugo c'e'? %s\n" (CicNotationParser.pp_value x);
-                    flush stdout
-                | None  -> prerr_endline "nooooo"
-              end
-           | _ -> assert false *)
-          end ;
           P.Sort `Prop)
     in
     CicNotationParser.print_l2_pattern ()