existential variables in goal supported

[helm.git] / helm / software / components / tactics / paramodulation / subst.ml

diff --git a/helm/software/components/tactics/paramodulation/subst.ml b/helm/software/components/tactics/paramodulation/subst.ml
index f738d2f63354a343c82b0416d5cd6cb69f7e3ded..819472a15485c0314da6228a3374f300d67d7e94 100644 (file)
--- a/helm/software/components/tactics/paramodulation/subst.ml
+++ b/helm/software/components/tactics/paramodulation/subst.ml
@@ -211,5 +211,6 @@ let merge_subst_if_possible = naif_merge_subst_if_possible;;
 
 let empty_subst = [];;
 
-let concat_substs x y = x @ y;;
+let concat x y = x @ y;;
+