let _ =
DisambiguateChoices.add_num_choice
("natural number",
- (fun _ num _ -> LibraryObjects.build_nat (int_of_string num)));
+ `Num_interp (fun num -> LibraryObjects.build_nat (int_of_string num)));
DisambiguateChoices.add_num_choice
("Coq natural number",
- (fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
+ `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
DisambiguateChoices.add_num_choice
("real number",
- (fun _ num _ -> HelmLibraryObjects.build_real (int_of_string num)));
+ `Num_interp (fun num -> HelmLibraryObjects.build_real (int_of_string num)));
DisambiguateChoices.add_num_choice
("binary positive number",
- (fun _ num _ ->
+ `Num_interp (fun num ->
let num = int_of_string num in
if num = 0 then
- raise (DisambiguateTypes.Invalid_choice (None, lazy "0 is not a valid positive number"))
+ raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number")))
else
HelmLibraryObjects.build_bin_pos num));
DisambiguateChoices.add_num_choice
("binary integer number",
- (fun _ num _ ->
+ `Num_interp (fun num ->
let num = int_of_string num in
if num = 0 then
HelmLibraryObjects.BinInt.z0