snapshot (first version with working pattern matching both 3->2 and 2->1)

[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 722748a96c42f896d05fce32147707017d4a723e..77135a977d04778312c676faf984ff0beddfa04a 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -89,10 +89,7 @@ let _ =
                 let time1 = Unix.gettimeofday () in
                 ignore
                   (CicNotationParser.extend l1 ?precedence ?associativity
-                    (fun env loc ->
-                      prerr_endline "ENV";
-                      prerr_endline (CicNotationPp.pp_env env);
-                      CicNotationFwd.instantiate_level2 env l2));
+                    (fun env loc -> CicNotationFwd.instantiate_level2 env l2));
                 let time2 = Unix.gettimeofday () in
                 print_endline "Extending pretty printer ..."; flush stdout;
                 let time3 = Unix.gettimeofday () in
@@ -135,7 +132,8 @@ let _ =
                 let t' = CicNotationRew.pp_ast t in
                 let time4 = Unix.gettimeofday () in
                 printf "pretty printing took %f seconds\n" (time4 -. time3);
-                print_endline (CicNotationPp.pp_term t'); flush stdout)
+                print_endline (CicNotationPp.pp_term t'); flush stdout
+                )
 (*                 CicNotationParser.print_l2_pattern ()) *)
         | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
         | 2 ->