| None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command"))
in
let ty_term,_ =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then ProofEngineTypes.apply_tactic
(P.apply_tac