removed a bad prerr_endline

[helm.git] / components / tactics / paramodulation / subst.mli

diff --git a/components/tactics/paramodulation/subst.mli b/components/tactics/paramodulation/subst.mli
index 3bbf7d00cb2f322b680d250f84f4e4fba6d18106..9c124d9633502900162b760365add3ee62a02f2f 100644 (file)
--- a/components/tactics/paramodulation/subst.mli
+++ b/components/tactics/paramodulation/subst.mli
@@ -39,5 +39,4 @@ val is_in_subst : int -> substitution -> bool
 val merge_subst_if_possible: 
   substitution -> substitution -> 
     substitution option
-val concat_substs: substitution -> substitution -> substitution
-
+val concat: substitution -> substitution -> substitution