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 e17d6cb7b68f16c5f4bac08b75fe91d3bdda4506..70502d1b28030650e0540348f5582b9b9ba06369 100644 (file)
--- 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];