let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
- let term,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
+ let term,_,metasenv'',_ = (* TASSI: FIXME what are we doning here?*)
+ CicRefine.type_of_aux' metasenv' context expr CicUniv.empty_ugraph
in
- Ok (term,metasenv'')
+ Ok (term,metasenv'') (* TASSI: whould we pass back the ugraph? *)
with
CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;