Errata to "An Intuitionistic Logic That Proves Markov's Principle", H. Herbelin ------------------------------------------------------------------------------- (April 2021) Typos ----- On Figure 2, "/\^_E^o" should be "/\^_E^i", and "pi_1 p" should be "pi_i p". Arguments of case, dest, efq were wrongly typeset in tt font. Page 4, bottom of column 1: - "catch_alpha only applies to proofs of forall-implication-formulas" should be "catch_alpha only applies to proofs of forall-implication-free formulas", - "one is sure that alpha does occur in V" should be "one is sure that alpha does _not_ occur in V". Thanks to Vincent Semaria for reporting.