calculation of the sort user to choose the rewriting principle fixed

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

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 9739f1ccf44ac84767adc0ea018210d601e3d75f..5df1d7d6f243222f4a7cedcaf57b726f8bf6db06 100644 (file)
--- 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