]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fourierR.ml
removed deadcode / fixed typos (thanks to ocaml 3.09)
[helm.git] / helm / ocaml / tactics / fourierR.ml
index 13dd9f410af6c74b2019842158a4a1b1a96a25c0..32dfb5db27ed2529000dcb39411ef0aae1e3c376 100644 (file)
@@ -941,8 +941,6 @@ let rec fourier (s_proof,s_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 *)