From cd99db7e082123b0e410d65f364f340aeb1af3d7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 30 Jun 2007 12:10:09 +0000 Subject: [PATCH] Spurious "we need to prove" at the beginning of Intros+LetTac are no longer generated. --- helm/software/components/content_pres/content2pres.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index a41ccc991..018497404 100644 --- 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 ([], -- 2.39.2