X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=5df1d7d6f243222f4a7cedcaf57b726f8bf6db06;hb=55c78a59b2127ecead99bb814a3ca519f8087053;hp=9739f1ccf44ac84767adc0ea018210d601e3d75f;hpb=2f4cf6f683207d7e755f8ba067f86c2f98f778fb;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 9739f1ccf..5df1d7d6f 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1277,10 +1277,11 @@ let fix_proof metasenv context all_implicits p =
 	  let metasenv,s = aux metasenv n s in
 	  let metasenv,t = aux metasenv (n+1) t in
 	    metasenv,Cic.Prod(name,s,t)
-      | Cic.LetIn(name,s,t) ->
+      | Cic.LetIn(name,s,ty,t) ->
 	  let metasenv,s = aux metasenv n s in
+	  let metasenv,ty = aux metasenv n ty in
 	  let metasenv,t = aux metasenv (n+1) t in
-	    metasenv,Cic.LetIn(name,s,t)	      
+	    metasenv,Cic.LetIn(name,s,ty,t)
       | Cic.Const(uri,ens) -> 
 	  let metasenv,ens =
 	    List.fold_right