None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
- let ty = CicTypeChecker.type_of_aux' metasenv context term in
- P.perforate context term ty (* P.perforate also sets the goal *)
+ let ty,_ = (* TASSI: FIXME ehhmmmm *)
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
+ P.perforate context term ty (* P.perforate also sets the goal *)
;;
exception FocusOnlyOnMeta;;
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
- let ty = CicTypeChecker.type_of_aux' metasenv context term in
- match term with
- Cic.Meta (n,_) -> P.goal := Some n
- | _ -> raise FocusOnlyOnMeta
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
+ match term with
+ Cic.Meta (n,_) -> P.goal := Some n
+ | _ -> raise FocusOnlyOnMeta
;;