]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/test_parser.ml
merged cic_notation with disambiguation: good luck!
[helm.git] / helm / ocaml / cic_notation / test_parser.ml
index 22d5c09fff2b8f72ffce424d4cce1fa8b9674f8d..df94eaa6f3c320e38cacfc4cfcb6725d22bda50b 100644 (file)
@@ -91,10 +91,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);