From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 9 Mar 2008 17:45:49 +0000 (+0000)
Subject: Performance improvement: let-ins should always be pushed to the context with
X-Git-Tag: make_still_working~5550
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d000041898471a4337a5e1af0f14ef2434d542b8;p=helm.git

Performance improvement: let-ins should always be pushed to the context with
their type (to avoid multiple re-typing).
---

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