Merge branch 'robbert/revert_475' into 'master'

Revert "Merge branch 'ralf/mangled' into 'master'"

See merge request !477

.gitlab-ci.yml

@@ -55,12 +55,14 @@ 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,9 +67,6 @@ 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

-(** Coq configuration for std++ (not meant to leak to clients) *)
+(** Coq configuration for std++ (not meant to leak to clients).
+If you are a user of std++, note that importing this file means
+you are implicitly opting-in to every new option we will add here
+in the future. We are *not* guaranteeing any kind of stability here.
+Instead our advice is for you to have your own options file; then
+you can re-export the std++ file there but if we ever add an option
+you disagree with you can easily overwrite it in one central location. *)
 (* Everything here should be [Export Set], which means when this
 file is *imported*, the option will only apply on the import site
 but not transitively. *)
@@ -12,13 +18,6 @@ Export Set Suggest Proof Using. *)
 that bullets and curly braces must be used to structure the proof. *)
 Export Set Default Goal Selector "!".
 
-(** Prevent using auto-generated names in proof scripts (or at least make it
-obvious when that happens) *)
-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.
 From stdpp Require Import options.