From f0e52c3d08c0ee4628ad6bbec32ad912dd35a2a4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 20 Jul 2006 15:10:24 +0000
Subject: [PATCH] trans chains even inside letins body

---
 .../tactics/paramodulation/equality.ml        | 20 +++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 2634752e7..368a80f5d 100644
--- 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 ->
-- 
2.39.2