trans chains even inside letins body

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 2634752e7aea7c65b818b7c7c1a5fd60c1b17496..368a80f5d7f03b8a5242fc828110b85cd2255b3b 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -422,16 +422,29 @@ let mk_feq uri_feq ty ty1 left pred right t =
   Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
 ;;
 
+let rec look_ahead aux = function
+  | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) as t
+        when LibraryObjects.is_eq_ind_URI uri_ind || 
+             LibraryObjects.is_eq_ind_r_URI uri_ind ->
+          let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+          let ty2,eq,lp,rp = open_pred pred in 
+          let hole = Cic.Implicit (Some `Hole) in
+          let ty2 = CicSubstitution.subst hole ty2 in
+          aux ty1 (CicSubstitution.subst other lp) (CicSubstitution.subst other rp) hole ty2 t
+  | Cic.Lambda (n,s,t) -> Cic.Lambda (n,s,look_ahead aux t)
+  | t -> t
+;;
+
 let contextualize uri ty left right t = 
   let hole = Cic.Implicit (Some `Hole) in
-  (* aux [uri] [ty] [left] [right] [ctx] [t] 
+  (* aux [uri] [ty] [left] [right] [ctx] [ctx_ty] [t] 
    * 
    * the parameters validate this invariant  
    *   t: eq(uri) ty left right
    * that is used only by the base case
    *
    * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
-   * ty_ctx is the type of ctx_d
+   * ctx_ty is the type of ctx
    *)
     let rec aux uri ty left right ctx_d ctx_ty = function
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
@@ -439,8 +452,7 @@ let contextualize uri ty left right t =
           let ty,l,r,p = open_sym ens tl in
           mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
       | Cic.LetIn (name,body,rest) ->
-          (* we should go in body *)
-          Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest)
+          Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty rest)
       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
         when LibraryObjects.is_eq_ind_URI uri_ind || 
              LibraryObjects.is_eq_ind_r_URI uri_ind ->