From 41c84b305a3e46a972f7fe955c300757a4cfb3ca 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 --- components/tactics/primitiveTactics.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index e17d6cb7b..70502d1b2 100644 --- a/components/tactics/primitiveTactics.ml +++ b/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