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

This reverts commit 6a7d163c, reversing
changes made to 40e5274f.

.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

@@ -12,13 +12,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.