X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Ftest_indexing.ml;h=5681a5d08725c1c05971c287e91d67d3aee33a87;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7391812f3d71b8c6028723edd50f0e1b3ccb219f;hpb=22d39afadb3027477e4a42c315ec10518cbf47ed;p=helm.git

diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
index 7391812f3..5681a5d08 100644
--- 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 ();;