| _ -> assert false
let get_types uri =
- match CicEnvironment.get_obj uri with
- | Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
+ let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
+ | Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,_) -> l
let name_of_inductive_type uri i =
let types = get_types uri in
in
let idref id t = Ast.AttributedTerm (`IdRef id, t) in
let rec aux =
-prerr_endline "Acic2ast.aux";
function
| Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
| Cic.AVar (id,uri,subst) ->
context
in
- let res = aux acic, ids_to_uris in
-prerr_endline "/Acic2ast.aux";
- res
+ aux acic, ids_to_uris
let _ = (** fill symbol_table *)
let add_symbol name uri =