From 8730af050d2d27d9aa0d4de42d3b0278a0a9ba6c Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 12:19:34 +0000
Subject: [PATCH] removed old broken code

---
 helm/ocaml/paramodulation/inference.ml | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
2.39.2