From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 20 Jul 2006 15:10:24 +0000 (+0000)
Subject: trans chains even inside letins body
X-Git-Tag: 0.4.95@7852~1167
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8dfe64de7854c787c1f226a11e7ed540b0e67d9f;p=helm.git

trans chains even inside letins body
---

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