X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagType.ml;h=9bae115df0594f38e0ba948a738e97b1f33cd029;hb=ae63e62aaf5659fe6b0e48cc4a4bdcf7b57318ad;hp=4ffa2e1f4cc7022a01ee53221ca34f63bcc2502c;hpb=fc15ad45208cc2e649fa435e547ecc757fe28481;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml
index 4ffa2e1f4..9bae115df 100644
--- a/helm/software/lambda-delta/basic_ag/bagType.ml
+++ b/helm/software/lambda-delta/basic_ag/bagType.ml
@@ -152,10 +152,10 @@ let rec b_type_of f g c x =
 	    in
 	    R.are_convertible f c w vv
 (* inserting a missing "modus ponens" *)
-	 | R.GRef (uri, vs) when U.eq uri I.imp ->
+	 | R.GRef (uri, vs) when U.eq uri I.imp && !R.ext = R.No ->
 	    L.log O.specs level (L.items1 "Rechecking coerced term");
 	    b_type_of f g c (mk_gref I.mp (vs @ [xv; xt]))
-	 | R.GRef (uri, vs) when U.eq uri I.all ->
+	 | R.GRef (uri, vs) when U.eq uri I.all && !R.ext = R.No ->
 	    L.log O.specs level (L.items1 "Rechecking coerced term");
 	    b_type_of f g c (mk_gref I.alle (vs @ [xt; xv]))
 	 | _                                    -> 
@@ -180,4 +180,3 @@ let rec b_type_of f g c x =
 and type_of f g c x =
    let f t u = L.unbox level; f t u in
    L.box level; b_type_of f g c x
-