X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicTypeChecker.ml;h=531705a3c2d40abf7d2699291e683b5da0b2e70f;hb=cbcd34fe15122eb9835a5226b98be1050b097d6a;hp=c67dc5343f622b0ce215c28c0ed5fa4dee3e99d8;hpb=a1b87ca1225a74b0d7b913e38c8ff6004737448b;p=helm.git

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index c67dc5343..531705a3c 100644
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/components/cic_proof_checking/cicTypeChecker.ml
@@ -1569,7 +1569,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 type_of_aux ~logger 
 	   ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 
        in
-       (CicSubstitution.subst s ty1),ugraph2
+       (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
    | C.Appl (he::tl) when List.length tl > 0 ->
        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
        let tlbody_and_type,ugraph2 = 
@@ -1963,7 +1963,8 @@ end;
 		    begin
 		      CicReduction.fdebug := -1 ;
 		      eat_prods ~subst context 
-			(CicSubstitution.subst hete t) tl ugraph1
+			(CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+                         tl ugraph1
 			(*TASSI: not sure *)
 		    end
 		  else