let tcl_fail a (proof,goal) =
match a with
- 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+ 1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical"))
| _ -> (proof,[goal])
;;
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
debug_pcontext s_context;
- let fhyp = String.copy "new_hyp_for_fourier" in
-
(* here we need to negate the thesis, but to do this we need to apply the
right theoreme,so let's parse our thesis *)