From eeed0d603ddadba6b5ee5041e87794051b9283dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Jun 2007 13:09:20 +0000 Subject: [PATCH] cut is now implemented building a letin and not a beta redex --- helm/software/components/tactics/primitiveTactics.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index e17d6cb7b..70502d1b2 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -409,11 +409,16 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: CicMkImplicit.identity_relocation_list_for_metavariable context in let newmeta1ty = CicSubstitution.lift 1 ty in +(* This is the pre-letin implementation let bo' = C.Appl [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; C.Meta (newmeta2,irl2)] in +*) + let bo' = + Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1)) + in let (newproof, _) = ProofEngineHelpers.subst_meta_in_proof proof metano bo' [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; -- 2.39.2