- scope management completed

[helm.git] / matita / components / binaries / matex / anticipate.ml

diff --git a/matita/components/binaries/matex/anticipate.ml b/matita/components/binaries/matex/anticipate.ml
index 1681d2d0355f99da04ca0153269ac6b8694b9d79..1081dffccfddb074a2d82addee90c222d743f1fb 100644 (file)
--- a/matita/components/binaries/matex/anticipate.ml
+++ b/matita/components/binaries/matex/anticipate.ml
@@ -29,7 +29,9 @@ let malformed s =
 let ok s =
    X.log ("anticipate: ok " ^ s)
 
-let not_prop1 c u = match (K.whd c (K.typeof c u)) with
+let typeof c t = K.whd c (K.typeof c t)
+
+let not_prop1 c u = match typeof c u with
    | C.Sort (C.Prop) -> false
    | C.Sort _        -> true
    | _               -> malformed "1"