let test_this mqi_handle uri_pred raw_term =
let empty_context = [] in
List.map
- (function (env, metasenv, cic_term) ->
+ (function (env, metasenv, cic_term,ugraph ) ->
let etype =
try
- CicPp.ppterm
- (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
+ let ty, _ =
+ (CicTypeChecker.type_of_aux' metasenv empty_context cic_term ugraph)
+ in
+ CicPp.ppterm ty
with _ -> "MALFORMED"
in
let ereduced =
etype = etype ^ "\n";
ereduced = ereduced ^ "\n";
}
- ) (BatchParser.parse mqi_handle ~uri_pred raw_term)
+ ) (BatchParser.parse mqi_handle ~uri_pred raw_term CicUniv.empty_ugraph)
let dump_environment filename =
try