let symbol_table = Hashtbl.create 1024
-let sort_of_string = function
- | "Prop" -> `Prop
- | "Set" -> `Set
- | "Type" -> `Type
- | "CProp" -> `CProp
- | _ -> 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
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
- | `Set | `Type -> `Pi
+ | `Set | `Type | `Meta -> `Pi
| `Prop | `CProp -> `Forall
in
idref id (Ast.Binder (binder_kind, (n, Some (aux s)), aux t))