]> matita.cs.unibo.it Git - helm.git/commitdiff
Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 30 Jun 2007 12:10:09 +0000 (12:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 30 Jun 2007 12:10:09 +0000 (12:10 +0000)
generated.

components/content_pres/content2pres.ml

index a41ccc99158a73562218887d2d786e57d903121e..018497404cf3277aef6f93c9636d07825eb8b427 100644 (file)
@@ -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 ([],