*)
let fails f a =
try
- let tmp = (f a) in
- false
+ ignore (f a);
+ false
with
_-> true
;;
apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
else
apply_tactic (Tacticals.then_
- ~start:( mk_tactic (fun status ->
- let (proof, goal) = status in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
+ ~start:(mk_tactic (apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt)))
~continuation:(tac_zero_infeq_pos gl (-n,d)))
status
in