let (_,c,t) = CicUtil.lookup_meta x menv in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable c in
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
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))
when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
pp true p
| Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p]
when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
pp true p
| Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p]
pp true p
| Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p]
when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->
pp true p
| Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p]
when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->