e ->
match e with
(Fail _)
- | (CicTypeChecker.TypeCheckerFailure (CicTypeChecker.NotWellTyped _))
- | (CicUnification.UnificationFailed) ->
+ | (CicTypeChecker.TypeCheckerFailure _)
+ | (CicUnification.UnificationFailure _) ->
warn (
"Tacticals.try_tactics failed with exn: " ^
Printexc.to_string e);
let prova_tac =
let apply_T_tac ~status:((proof,goal) as status) =
let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
let rel =
let rec find n =
function