even outside fix_arity (in cicRefine/eat_prods)
try
match t with
| Cic.Sort s -> Sort s
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 _ ->
| Cic.Appl (t::_)
| t -> Uri (CicUtil.uri_of_term t)
with Invalid_argument _ ->