X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=db185b421b040e5a1f8cbb63677c399b43114c7e;hb=d35d134356645a09eb72db6e484f3df583123af1;hp=23347e24ca0eb55d98d25c247bb2ba9e2eb15b11;hpb=e701ae61ea78b5bcbc8919ccb51f4f2ada8c5f23;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 23347e24c..db185b421 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -330,6 +330,7 @@ let meta_convertibility t1 t2 =
 ;;
 
 
+(*
 let replace_metas (* context *) term =
   let module C = Cic in
   let rec aux = function
@@ -420,6 +421,7 @@ let rec restore_subst (* context *) subst =
        i, (c, restore_metas (* context *) t, ty))
     subst
 ;;
+*)
 
 
 let rec check_irl start = function