[printer] Pp problem

[ejgallego]

This code by Mukesh Tiwari doesn't print properly:

From Coq Require Import NArith Utf8
    Bool Init.Byte Psatz Strings.Byte. 

Open Scope N_scope.
Definition np_total (np : N):  (np <? 256 = true) ->  byte.
Proof.
  intros H.
  refine(match (np <? 256) as b return ∀ mp, np = mp -> 
      (mp <? 256) = b -> _ with 
   | true => fun mp Hmp Hmpt => 
      match of_N mp as npt return _ = npt -> _ with 
      | Some x => fun _ => x
      | None => fun Hf => _  
      end eq_refl
   | false => fun mp Hmp Hmf => _
  end np eq_refl eq_refl).
  abstract(
  apply of_N_None_iff in Hf;
  apply N.ltb_lt in Hmpt; intuition nia).
  abstract (subst; congruence).
Defined.


Lemma np_true_tmp : forall np (Ha : np <? 256 = true) x, 
  of_N np = Some x -> np_total np Ha = x.
Proof.
  intros * Hb; unfold np_total.

[ejgallego]

See coq-community/vscoq#670 for screenshots (tho the second screenshot doesn't reflect how it should print either I think)

[ejgallego]

That's the correct rendering: