-let nat_URI = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind"
-
-let zero = Cic.MutConstruct (nat_URI,0,1,[])
-let succ = Cic.MutConstruct (nat_URI,0,2,[])
-
-let build_nat n =
- if n < 0 then assert false;
- let rec aux = function
- | 0 -> zero
- | n -> Cic.Appl [ succ; (aux (n - 1)) ]
- in
- aux n
+let nat_URI () =
+ try Some (List.hd !nat_URIs_ref) with Failure "hd" -> None
+let is_nat_URI uri =
+ List.exists (fun nat -> UriManager.eq nat uri) !nat_URIs_ref