X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=2447fe1ef64d7c10e9ab70d80da9da79d92588f0;hb=10d3194c1b42dfa72e51000ff2cc217f937b43ac;hp=47acc7c583a30cc789d96439852dfc5361b70aa2;hpb=07d2ed390e9e19420aa8e12a3ccac1d68cbd928d;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 47acc7c58..2447fe1ef 100644
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -444,13 +444,13 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
      raise 
        (ProofEngineTypes.Fail (lazy
          "You can't letin a term containing the current goal"));
-    let _,_ =
+    let tty,_ =
       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let fresh_name =
       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
      let context_for_newmeta =
-      (Some (fresh_name,C.Def (term,None)))::context in
+      (Some (fresh_name,C.Def (term,Some tty)))::context in
      let irl =
       CicMkImplicit.identity_relocation_list_for_metavariable
        context_for_newmeta