]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/test_parser.ml
refactored modules structure
[helm.git] / helm / ocaml / cic_notation / test_parser.ml
index bcb7e661b7e37936b993c9c0f40ddc7785171d5d..d39c0ff94d86526e84e206dba739b38655e9480f 100644 (file)
@@ -26,7 +26,6 @@
 open Printf
 
 let _ =
-  CicNotationEnv.set_pp_term CicNotationPp.pp_term;
   let module P = CicNotationPt in
   let level = ref ~-1 in
   let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in
@@ -86,7 +85,7 @@ let _ =
                     (fun env loc ->
                       prerr_endline "ENV";
                       prerr_endline (CicNotationPp.pp_env env);
-                      CicNotationEnv.instantiate env l2)))
+                      CicNotationSubst.instantiate_level2 env l2)))
 (*                 CicNotationParser.print_l2_pattern ()) *)
         | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
         | 2 ->