+module C = Cic
+module Obj = LibraryObjects
+module DT = DisambiguateTypes
+
+let error msg =
+ raise (DT.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
+
+let build_nat o s str =
+ let n = int_of_string str in
+ if n < 0 then error (str ^ " is not a valid natural number number") else
+ let rec aux n = if n = 0 then o () else s (aux (pred n)) in
+ aux n
+
+let interp_natural_number num =
+ let nat_URI = match Obj.nat_URI () with
+ | Some uri -> uri
+ | None -> error "no default natural numbers"
+ in
+ let o () = C.MutConstruct (nat_URI,0,1,[]) in
+ let s t = C.Appl [C.MutConstruct (nat_URI,0,2,[]); t] in
+ build_nat o s num
+