- let _,_,oldty = CicUtil.lookup_meta g metasenv in
- let _,_,newty = CicUtil.lookup_meta g1 metasenv' in
- if oldty = newty then
+ let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+ let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+ if oldty = newty && oc = nc then