Skip to content

Name mangling light causes noise in printing

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).