debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
debug_pcontext s_context;
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
debug_pcontext s_context;
(* here we need to negate the thesis, but to do this we need to apply the
right theoreme,so let's parse our thesis *)
(* here we need to negate the thesis, but to do this we need to apply the
right theoreme,so let's parse our thesis *)
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic