let module C = Cic in
let rec aux k =
function
- C.Rel m as t -> t,[m - k]
+ C.Rel m as t -> t,[k - m]
| C.Var (uri,exp_named_subst) ->
let exp_named_subst',rels =
List.fold_right
in
C.Meta(i,l'),rels
| C.Sort _ as t -> t,[]
- | C.Implicit as t -> t,[]
+ | C.Implicit _ as t -> t,[]
| C.Cast (te,ty) ->
let te',rels1 = aux k te in
let ty',rels2 = aux k ty in
let n' =
match n with
C.Anonymous ->
- if List.mem k rels2 then assert false else C.Anonymous
+ if List.mem k rels2 then
+(
+ prerr_endline "If this happens often, we can do something about it (i.e. we can generate a new fresh name; problem: we need the metasenv and context ;-(. Alternative solution: mk_implicit does not generate entries for the elements in the context that have no name" ;
+ C.Anonymous
+)
+ else
+ C.Anonymous
| C.Name _ as n ->
if List.mem k rels2 then n else C.Anonymous
in