The branching-time logic BCTL* is obtained by referring to a more general semantics than that of CTL* ; namely we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard CTL* validity semantics. In this talk, I will present a sound and complete (labeled) natural deduction system for the until-free version of BCTL* and I will show that it enjoys some good proof-theoretical properties.