in
match opened with
| [g1] ->
- 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
raise (PET.Fail msg)
else
ostatus