enable name-mangling-light

For instance, the proof state after the intros. in lookup_total_app_l now looks like

  A : Type
  __Inhabited : Inhabited A
  l1, l2 : list A
  i : nat
  __H : i < length l1
  ============================
  (l1 ++ l2) !!! i = l1 !!! i

I like it. :) I think we can just always enable this and not have anything extra on CI; we will hopefully notice when proof scripts contain such an identifier starting with __.

Why __ and not just _?

In ssreflect it's actually impossible to use the _ names, I understand that this is not the case here?

added 2 commits

• bb8cfd6d - enable name-mangling-light
• 11902aaa - changelog

Compare with previous version

resolved all threads

I think we can merge this, feel free to press the button when you wish.

merged

mentioned in commit 6a7d163c

mentioned in issue #184

mentioned in merge request !477 (merged)