From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 12:19:34 +0000 (+0000)
Subject: removed old broken code
X-Git-Tag: V_0_7_2~126
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8730af050d2d27d9aa0d4de42d3b0278a0a9ba6c;p=helm.git

removed old broken code
---

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