]> matita.cs.unibo.it Git - helm.git/commitdiff
carr_of_term now returns Fun if a Prod is encountered
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 12 Oct 2006 16:10:53 +0000 (16:10 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 12 Oct 2006 16:10:53 +0000 (16:10 +0000)
components/library/coercDb.ml

index 9a1fdb0ea85de8434cf529ccfa183151960fb455..ac57aa40a82b3f4fde03e07e588646ab10f40871 100644 (file)
@@ -40,7 +40,8 @@ let db = ref []
 let coerc_carr_of_term t =
  try
   match t with
-     Cic.Sort s -> Sort s
+   | Cic.Sort s -> Sort s
+   | Cic.Prod _ -> Fun 0
    | Cic.Appl (t::_)
    | t -> Uri (CicUtil.uri_of_term t)
  with Invalid_argument _ ->