snapshot

[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..5b42822c22b218d2495b4f32fe9d038f8a113ff3 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
@@ -106,13 +103,14 @@ let _ =
             | P.Interpretation (l2, l3) ->
                 print_endline "Adding interpretation ..."; flush stdout;
                 let time1 = Unix.gettimeofday () in
-                ignore (CicNotationRew.add_interpretation l2 l3);
+(*                 ignore (CicNotationRew.add_interpretation l2 l3); *)
                 let time2 = Unix.gettimeofday () in
                 printf "done (patterns compilation took %f seconds)\n"
                   (time2 -. time1);
                 flush stdout
             | P.Render uri ->
-                let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                assert false
+(*                 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                 let annobj, _, _, id_to_sort, _, _, _ =
                   Cic2acic.acic_object_of_cic_object obj
                 in
@@ -135,7 +133,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 ->