]> matita.cs.unibo.it Git - helm.git/commitdiff
coercions from funclass are not supported
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Aug 2007 13:13:56 +0000 (13:13 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 30 Aug 2007 13:13:56 +0000 (13:13 +0000)
helm/software/components/library/coercDb.ml

index aec6dd5795bb9051adf78ce7336cc5f34cef6193..1f3874912b93ff231ca48563a1c9ad04d6f9e23c 100644 (file)
@@ -41,7 +41,7 @@ let coerc_carr_of_term t =
  try
   match t with
    | Cic.Sort s -> Sort s
-   | Cic.Prod _ -> Fun 0
+   | Cic.Prod _ -> assert false
    | Cic.Appl (t::_)
    | t -> Uri (CicUtil.uri_of_term t)
  with Invalid_argument _ ->