X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsubst.ml;h=fb8e3b78e25266a473fc3d0d9b9f5d59ce7a06e7;hb=1c9b8f3ba2c86446d44160ae494bc85624bc5eaf;hp=7e8ab8b185235b30a5e8a5aaef29ece17752ee5d;hpb=942023d1f147318b7869f40fb1556c2d69f3d731;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/subst.ml b/helm/software/components/tactics/paramodulation/subst.ml
index 7e8ab8b18..fb8e3b78e 100644
--- a/helm/software/components/tactics/paramodulation/subst.ml
+++ b/helm/software/components/tactics/paramodulation/subst.ml
@@ -94,7 +94,7 @@ let naif_apply_subst lift subst term =
     | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
     | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
     | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
-    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+    | Cic.LetIn (n,s,ty,t) -> Cic.LetIn (n, aux k s, aux k ty, aux (k+1) t)
     | Cic.Appl [] -> assert false
     | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
     | Cic.Const (uri,exp_named_subst) ->