- Removed old proofs

[helm.git] / helm / software / components / tactics / paramodulation / inference.mli

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 08d1c8f266010354deb9c48dbcf86d9c16fc7c1d..9bfb84cb21f8ea7f0164845544ba556a02c51e0d 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -30,7 +30,7 @@ val matching:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> 
   Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+    Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
@@ -40,7 +40,7 @@ val unification:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> 
   Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+    Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**