* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open DisambiguateTypes
-exception Invalid_choice
exception Choice_not_found of string Lazy.t
let num_choices = ref []
in
try
List.combine names cic_args
- with Invalid_argument _ -> raise Invalid_choice
+ with Invalid_argument _ ->
+ raise (Invalid_choice (lazy "The notation expects a different number of arguments"))
in
- CicNotationFwd.instantiate_appl_pattern env' appl_pattern)
+ TermAcicContent.instantiate_appl_pattern env' appl_pattern)
let lookup_symbol_by_dsc symbol dsc =
try
mk_choice
(List.find
(fun (dsc', _, _) -> dsc = dsc')
- (CicNotationRew.lookup_interpretations symbol))
- with CicNotationRew.Interpretation_not_found | Not_found ->
+ (TermAcicContent.lookup_interpretations symbol))
+ with TermAcicContent.Interpretation_not_found | Not_found ->
raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))