we started the support for naive sort inclusion

[helm.git] / helm / software / lambda-delta / basic_ag / bagType.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml
index 4ffa2e1f4cc7022a01ee53221ca34f63bcc2502c..9bae115df0594f38e0ba948a738e97b1f33cd029 100644 (file)
--- 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
-