From d000041898471a4337a5e1af0f14ef2434d542b8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 9 Mar 2008 17:45:49 +0000 Subject: [PATCH] Performance improvement: let-ins should always be pushed to the context with their type (to avoid multiple re-typing). --- helm/software/components/tactics/primitiveTactics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2