X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.ml;h=14ddf7c8631b5054aca10a8accc0268e9c12b05f;hb=699d76ddae765f0a927648cddf624b540743f225;hp=e0dc18d05f7146e9bf0125265eb9ef4aaa41e660;hpb=396a578b680e7fdb9d262822184e52f0d4d5086b;p=helm.git

diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml
index e0dc18d05..14ddf7c86 100644
--- a/components/library/coercDb.ml
+++ b/components/library/coercDb.ml
@@ -41,7 +41,10 @@ let coerc_carr_of_term t =
  try
   match t with
    | Cic.Sort s -> Sort s
-   | Cic.Prod _ -> assert false
+   | Cic.Prod _ -> Fun 0 
+     (* BUG: this should be the real arity. The computation
+      requires menv, context etc.., but since carrs are compared discharging Fun
+      arity... it works *)
    | Cic.Appl (t::_)
    | t -> Uri (CicUtil.uri_of_term t)
  with Invalid_argument _ ->
@@ -180,7 +183,6 @@ let add_coercion (src,tgt,u,saturations) =
       if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
         let l' = List.map
           (fun (x,n,saturations') ->
-            assert (saturations=saturations');
             if UriManager.eq u x then
              (x,n+1,saturations)
             else