let symbol_table = Hashtbl.create 1024
-let sort_of_string = function
- | "Prop" -> `Prop
- | "Set" -> `Set
- | "Type" -> `Type
- | "CProp" -> `CProp
- | "?" -> `Meta
- | _ -> assert false
-
let get_types uri =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
let register_uri id uri = Hashtbl.add ids_to_uris id uri in
let sort_of_id id =
try
- sort_of_string (Hashtbl.find ids_to_inner_sorts id)
+ Hashtbl.find ids_to_inner_sorts id
with Not_found -> assert false
in
let idref id t = Ast.AttributedTerm (`IdRef id, t) in