X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicSubstitution.ml;h=a4340583efc8b1f98cbacfdb58a7f94efa8249a9;hb=57977d3ced75bb9d523280bcfd6e4bcfb07ba83e;hp=a30a036cb42dc7726c1720906d706f903b0fcf30;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_proof_checking/cicSubstitution.ml b/components/cic_proof_checking/cicSubstitution.ml
index a30a036cb..a4340583e 100644
--- a/components/cic_proof_checking/cicSubstitution.ml
+++ b/components/cic_proof_checking/cicSubstitution.ml
@@ -108,7 +108,12 @@ let lift n t =
    lift_from 1 n t
 ;;
 
-let subst arg =
+(* subst t1 t2                                                         *)
+(* substitutes [t1] for [Rel 1] in [t2]                                *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes  *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true.                          *)
+let rec subst ?(avoid_beta_redexes=false) arg =
  let rec substaux k =
   let module C = Cic in
    function
@@ -144,6 +149,12 @@ let subst arg =
         begin
          match substaux k he with
             C.Appl l -> C.Appl (l@tl')
+            (* Experimental *)
+          | C.Lambda (_,_,bo) when avoid_beta_redexes ->
+             (match tl' with
+                 [] -> assert false
+               | [he] -> subst ~avoid_beta_redexes he bo
+               | he::tl -> C.Appl (subst he bo::tl))
           | _ as he' -> C.Appl (he'::tl')
         end
     | C.Appl _ -> assert false