let module U = UriManager in
let module P = PrimitiveTactics in
let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then P.apply_tac
~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status