Spurious "we need to prove" at the beginning of Intros+LetTac are no longer

generated.

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index a41ccc99158a73562218887d2d786e57d903121e..018497404cf3277aef6f93c9636d07825eb8b427 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -290,11 +290,8 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
           else  
             let prequel =
               if
-               (match skip_initial_lambdas_internal with
-                   None
-                 | Some (`Later _) -> true
-                 | Some (`Now _) -> false)
-               && conclude.Con.conclude_method = "Intros+LetTac"
+               (not is_top_down) &&
+                conclude.Con.conclude_method = "Intros+LetTac"
               then
                 let name = get_name name in
                  [B.V ([],