Skip to content
Snippets Groups Projects

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

Merged Revert "Merge branch 'ralf/mangled' into 'master'"
robbert/revert_475 into master
All threads resolved!
Merged Robbert Krebbers requested to merge robbert/revert_475 into master
All threads resolved!

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

See #184

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Ralf Jung resolved all threads

    resolved all threads

  • Ralf Jung added 1 commit

    added 1 commit

    • d1dfd948 - warn against importing the options file

    Compare with previous version

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers mentioned in commit f34a9e18

    mentioned in commit f34a9e18

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Author Owner

    @iris-users This MR reverts !475 (merged):

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

    See https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Noisy.20printing.20with.20name.20mangling.20light for further discussion.

    • Please register or sign in to reply