(** raised by lookup_XXXX below *)
exception Choice_not_found of string Lazy.t
- (** register a new number choice *)
-val nadd_num_choice: NCic.term codomain_item -> unit
-
(** {2 Choices lookup}
* for user defined aliases *)
* @param dsc description (1st component of codomain_item)
*)
val lookup_symbol_by_dsc:
+ #Interpretations.status ->
mk_appl: ('term list -> 'term) ->
mk_implicit: (bool -> 'term) ->
term_of_nref: (NReference.reference -> 'term) ->