From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jun 2007 13:09:20 +0000 (+0000)
Subject: cut is now implemented building a letin and not a beta redex
X-Git-Tag: make_still_working~6247
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eeed0d603ddadba6b5ee5041e87794051b9283dd;p=helm.git

cut is now implemented building a letin and not a beta redex
---

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];