ocaml 3.09 transition

[helm.git] / helm / ocaml / paramodulation / test_indexing.ml

diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
index 7391812f3d71b8c6028723edd50f0e1b3ccb219f..5681a5d08725c1c05971c287e91d67d3aee33a87 100644 (file)
--- a/helm/ocaml/paramodulation/test_indexing.ml
+++ b/helm/ocaml/paramodulation/test_indexing.ml
@@ -210,11 +210,11 @@ let test_refl () =
     ]
   ] in
   let ens = [
-    (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
+    (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
      C.Rel 4);
-    (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
+    (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
      C.Rel 3);
-    (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
+    (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
      C.Rel 2);    
   ] in
   let term2 = C.Appl [
@@ -231,10 +231,21 @@ let test_refl () =
   Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty); 
 ;;
 
+
+let test_lib () =
+  let uri = Sys.argv.(1) in
+  let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in
+  let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+  Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t);
+  Printf.printf "type: %s\n" (CicPp.ppterm ty);
+;;
+
+
 (* differing ();; *)
 (* next_after ();; *)
 (* discrimination_tree_test ();; *)
 (* path_indexing_test ();; *)
 (* test_subst ();; *)
 Helm_registry.load_from "../../matita/matita.conf.xml";
-test_refl ();;
+(* test_refl ();; *)
+test_lib ();;