- ground_2: support for relocation updated

[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..47fc2cae11a9f1cdf398f35930457e6f95c16f4e 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"
@@ -119,7 +121,6 @@ try
 with
    | T.TypeCheckerFailure s
    | T.AssertFailure s           -> malformed (Lazy.force s)
-   | Invalid_argument "List.nth" -> malformed "4" (* to be removed *)
 
 let proc_fun c =
    let r, s, i, u, t = c in