+
+let disambiguate_cic_appl_pattern status args =
+ let rec disambiguate =
+ function
+ NotationPt.ApplPattern l ->
+ NotationPt.ApplPattern (List.map disambiguate l)
+ | NotationPt.VarPattern id
+ when not
+ (List.exists
+ (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
+ ->
+ let item = DisambiguateTypes.Id id in
+ begin
+ try
+ match
+ DisambiguateTypes.Environment.find item
+ status#disambiguate_db.aliases
+ with
+ GrafiteAst.Ident_alias (_, uri) ->
+ NotationPt.NRefPattern (NReference.reference_of_string uri)
+ | _ -> assert false
+ with Not_found ->
+ prerr_endline
+ ("LexiconEngine.eval_command: domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item));
+ dump_aliases prerr_endline "" status;
+ raise
+ (Failure
+ ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
+ end
+ | p -> p
+ in
+ disambiguate
+;;