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 47acc7c583a30cc789d96439852dfc5361b70aa2..2447fe1ef64d7c10e9ab70d80da9da79d92588f0 100644 (file)
--- 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