X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=9baf829ea940d2bad3c61d71ebfdea8781043f34;hb=be16471f978380deb789b3b70c92d998addbb350;hp=5fb8d4ae1eb56f88522cb14133c1a7c846a60e69;hpb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;p=helm.git

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 5fb8d4ae1..9baf829ea 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -571,7 +571,7 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres
 
 module C = Cic
 
-let letout_tac () =
+let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
    let letout_tac (proof, goal) =