X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Futils.ml;h=86c9c1430105e0948c4ba3274284b9b9b03caded;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;hp=a85ccc674220482c782598f26d1d1d1e8e4b9394;hpb=b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index a85ccc674..86c9c1430 100644
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/components/tactics/paramodulation/utils.ml
@@ -114,6 +114,8 @@ let rec remove_local_context =
     | Cic.Meta (i,_) -> Cic.Meta (i,[])
     | Cic.Appl l ->
        Cic.Appl(List.map remove_local_context l)
+    | Cic.Prod (n,s,t) -> 
+       Cic.Prod (n,remove_local_context s, remove_local_context t)
     | t -> t