initial import of standalone matitaprover binary

[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 7e8ab8b185235b30a5e8a5aaef29ece17752ee5d..fb8e3b78e25266a473fc3d0d9b9f5d59ce7a06e7 100644 (file)
--- 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) ->