snapshort

[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 5b42822c22b218d2495b4f32fe9d038f8a113ff3..98716ad8663c75269cbca5ac5b7290a4c2d0a2a9 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -26,8 +26,8 @@
 open Printf
 
 let _ =
-  Helm_registry.load_from "test_parser.conf.xml";
-  Http_getter.init ()
+  Helm_registry.load_from "test_parser.conf.xml"
+(*   Http_getter.init () *)
 
 let _ =
   let module P = CicNotationPt in
@@ -103,14 +103,13 @@ 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 ->
-                assert false
-(*                 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                 let annobj, _, _, id_to_sort, _, _, _ =
                   Cic2acic.acic_object_of_cic_object obj
                 in
@@ -133,7 +132,7 @@ 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)