enable name-mangling-light

.gitlab-ci.yml

@@ -55,14 +55,12 @@ build-coq.8.17.0-mr:
   variables:
     OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
-    MANGLE_NAMES: "1"
 
 build-coq.8.16.1:
   <<: *template
   variables:
     OPAM_PINS: "coq version 8.16.1"
     DENY_WARNINGS: "1"
-    MANGLE_NAMES: "1"
     CI_COQCHK: "1"
     OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"

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.