Merge branch 'ralf/mangled' into 'master'

enable name-mangling-light

See merge request iris/stdpp!475

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

CHANGELOG.md

@@ -67,6 +67,9 @@ longer supported by this release.
   (`map_fold` used to be derived from `map_to_list`.) This makes it possible to
   use `map_fold` in nested-recursive definitions on maps. For example,
   `Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
+- Enable 'light' name mangling in `stdpp.options`, which prefixes auto-generated
+  names with `__`. This only affects developments that explicitly opt-in to
+  following the std++ configuration by importing `stdpp.options`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

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.