]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/test_parser.ml
snapshot (the thing on the doorstep)
[helm.git] / helm / ocaml / cic_notation / test_parser.ml
index d39c0ff94d86526e84e206dba739b38655e9480f..6e0160e7a9ede006e5f2156501eaa96db682d7c6 100644 (file)
@@ -85,7 +85,7 @@ let _ =
                     (fun env loc ->
                       prerr_endline "ENV";
                       prerr_endline (CicNotationPp.pp_env env);
-                      CicNotationSubst.instantiate_level2 env l2)))
+                      CicNotationFwd.instantiate_level2 env l2)))
 (*                 CicNotationParser.print_l2_pattern ()) *)
         | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
         | 2 ->