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

stdpp/options.v

@@ -7,6 +7,10 @@ Export Set Default Proof Using "Type".
 (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
 Export Set Suggest Proof Using. *)
 Export Set Default Goal Selector "!".
+Export Set Mangle Names.
+Export Set Mangle Names Light.
+(** Make these names stand out more, in case one does end up in the proof script. *)
+Export Set Mangle Names Prefix "__".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.