]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/basic_ag/bagType.ml
- initial support for abstractions with explicit levels
[helm.git] / helm / software / lambda-delta / src / basic_ag / bagType.ml
index d92e232721ebad256cfb29e4c916919e4b746726..1314218d39f3f5933423a8cc5907da70cfbf7d31 100644 (file)
@@ -65,7 +65,7 @@ let rec b_type_of f st c x =
       Z.get f c i
    | Z.GRef uri                  ->
       let f = function
-         | _, _, E.Abst w               -> f x w
+         | _, _, E.Abst (_, w)          -> f x w
         | _, _, E.Abbr (Z.Cast (w, v)) -> f x w
         | _, _, E.Abbr _               -> assert false
         | _, _, E.Void                 -> assert false