in
(match ty with
C.Sort C.Type as s ->
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
let fresh_meta = !next_fresh_meta in
let fresh_meta' = fresh_meta + 1 in
next_fresh_meta := !next_fresh_meta + 2 ;
- let subst_item = uri,C.Meta (fresh_meta',irl) in
+ let subst_item = uri,C.Meta (fresh_meta',[]) in
newmetasenvfragment :=
(fresh_meta,[],C.Sort C.Type) ::
(fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;