"The notation " ^ dsc ^ " expects more arguments")))
in
let combined =
- TermAcicContent.instantiate_appl_pattern
+ Interpretations.instantiate_appl_pattern
~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref env' appl_pattern
in
match rest with
| _::_ -> mk_appl (combined::rest))
let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol dsc =
- let interpretations = TermAcicContent.lookup_interpretations ~sorted:false symbol in
+ let interpretations = Interpretations.lookup_interpretations ~sorted:false symbol in
try
mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref
(List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
- with TermAcicContent.Interpretation_not_found | Not_found ->
+ with Interpretations.Interpretation_not_found | Not_found ->
raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))
let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc