]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/test_parser.ml
- synced notation pretty printing with parsing syntax
[helm.git] / helm / ocaml / cic_notation / test_parser.ml
index 22d5c09fff2b8f72ffce424d4cce1fa8b9674f8d..62b0ae32bd585ca0551ca1e3d4d851ddf85b05c5 100644 (file)
@@ -76,6 +76,7 @@ let process_stream ?(ignore_exn = false) istream =
             G.Notation (_, l1, associativity, precedence, l2))) ->
               prerr_endline "Extending parser ..."; flush stdout;
               prerr_endline (CicNotationPp.pp_term l1) ;
+              prerr_endline (CicNotationPp.pp_term l2) ;
               prerr_endline (sprintf "Found keywords: %s"
                 (String.concat " " (CicNotationUtil.keywords_of_term l1)));
               let time1 = Unix.gettimeofday () in
@@ -91,10 +92,10 @@ let process_stream ?(ignore_exn = false) istream =
                         "extending pretty printer took %f)\n")
                         (time2 -. time1) (time4 -. time3);
                       flush stdout
-          | G.Executable (_, G.Command (_, G.Interpretation (_, l2, l3))) ->
+          | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) ->
               prerr_endline "Adding interpretation ..."; flush stdout;
               let time1 = Unix.gettimeofday () in
-                ignore (CicNotationRew.add_interpretation l2 l3);
+                ignore (CicNotationRew.add_interpretation id l2 l3);
                 let time2 = Unix.gettimeofday () in
                   printf "done (patterns compilation took %f seconds)\n"
                     (time2 -. time1);