Name mangling light causes noise in printing
View options
From stdpp Require Import options.
Check forall x, x = 0.
(** Prints forall __x : nat, __x = 0 *)This becomes worse when considering goals with quantifiers:
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
revert l2.
(* Prints ∀ __l2 : list A, (∀ __i : nat, l1 !! __i = __l2 !! __i) → l1 = __l2 *)This is totally unreadable.
Is there a way to fix this, or does this mean we should revert !475 (merged).