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 _ ->
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