let (_,c,t) = CicUtil.lookup_meta x menv in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable c in
- (x,(c,Cic.Meta(y,irl),t))
+ (y,(c,Cic.Meta(x,irl),t))
with CicUtil.Meta_not_found _ ->
try
let (_,c,t) = CicUtil.lookup_meta y menv in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable c in
- (y,(c,Cic.Meta(x,irl),t))
+ (x,(c,Cic.Meta(y,irl),t))
with CicUtil.Meta_not_found _ -> assert false) l in
Some subst
with NotMetaConvertible ->