Add feature to add name mangling suffixes

boot/usage.ml

@@ -85,7 +85,8 @@ let print_usage_common co command =
 \n  -allow-rewrite-rules   allows declaring symbols and rewrite rules\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
-\n  -mangle-names x        mangle auto-generated names using prefix x\
+\n  -mangle-names-prfx x   mangle auto-generated names using prefix x\
+\n  -mangle-names-sffx x   mangle auto-generated names using suffix x\
 \n  -set \"Foo Bar\"         enable Foo Bar (as Set Foo Bar. in a file)\
 \n  -set \"Foo Bar=value\"   set Foo Bar to value (value is interpreted according to Foo Bar's type)\
 \n  -unset \"Foo Bar\"       disable Foo Bar (as Unset Foo Bar. in a file)\

doc/sphinx/practical-tools/coq-commands.rst

@@ -475,13 +475,20 @@ and ``rocq repl``, unless stated otherwise:
 :-type-in-type: Collapse the universe hierarchy of Rocq.
 
   .. warning:: This makes the logic inconsistent.
-:-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace
+:-mangle-names-prfx *ident*: *Experimental.* Do not depend on this option. Replace
   Rocq's auto-generated name scheme with names of the form *ident0*, *ident1*,
   etc. Within Rocq, the :flag:`Mangle Names` flag turns this behavior on,
   and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature
   is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
+:-mangle-names-sffx *ident*: *Experimental.* Do not depend on this option. Replace
+  Rocq's auto-generated name scheme with names of the form *ident0*, *ident1*,
+  etc. Within Rocq, the :flag:`Mangle Names` flag turns this behavior on,
+  and the :opt:`Mangle Names Suffix` option sets the suffix to use. This feature
+  is intended to be used as a linter for developments that want to be robust to
+  changes in the auto-generated name scheme. The options are provided to
+  facilitate tracking down problems.
 :-set *string*: Enable flags and set options. *string* should be
    :n:`@setting_name=value`, the value is interpreted according to the
    type of the option. For flags :n:`@setting_name` is equivalent to

engine/namegen.ml

@@ -220,7 +220,7 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
 
 (* Introduce a mode where auto-generated names are mangled
    to test dependence of scripts on auto-generated names.
-   We also supply a version which only adds a prefix. *)
+   We also supply a version which adds a prefix/suffix. *)
 
 let { Goptions.get = get_mangle_names } =
   Goptions.declare_bool_option_and_ref
@@ -234,19 +234,28 @@ let { Goptions.get = get_mangle_names_light } =
     ~value:false
     ()
 
-let { Goptions.get = mangle_names_prefix } =
-  Goptions.declare_interpreted_string_option_and_ref
-    ~key:["Mangle";"Names";"Prefix"]
-    ~value:("_")
-    (fun x ->
+let _fix_check x =
       Id.to_string
       (try
          Id.of_string x
        with
        | CErrors.UserError _ ->
          CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))
       )
-    )
+
+let { Goptions.get = mangle_names_prefix } =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~key:["Mangle";"Names";"Prefix"]
+    ~value:("_")
+    _fix_check
+    (fun x -> x)
+    ()
+
+let { Goptions.get = mangle_names_suffix } =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~key:["Mangle";"Names";"Suffix"]
+    ~value:("_")
+    _fix_check
     (fun x -> x)
     ()
 
@@ -255,10 +264,11 @@ let { Goptions.get = mangle_names_prefix } =
 
 let mangle_id id =
   let prfx = mangle_names_prefix () in
+  let sffx = mangle_names_suffix () in
   if get_mangle_names () then
     if get_mangle_names_light () then
-      Id.of_string (prfx ^ Id.to_string id)
-    else Id.of_string (prfx ^ "0")
+      Id.of_string (prfx ^ Id.to_string id ^ sffx)
+    else Id.of_string (prfx ^ "0" ^ sffx)
   else id
 
 (* Looks for next "good" name by lifting subscript *)

sysinit/coqargs.ml

@@ -304,10 +304,14 @@ let parse_args ~init arglist : t * string list =
     |"-load-vernac-source"|"-l" ->
       add_load_vernacular oval (next ())
 
-    |"-mangle-names" ->
+    |"-mangle-names-prfx" ->
       let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in
       add_set_option oval ["Mangle"; "Names"; "Prefix"] (OptionSet(Some(next ())))
 
+    |"-mangle-names-sffx" ->
+      let oval = add_set_option oval ["Mangle"; "Names"] (OptionSet None) in
+      add_set_option oval ["Mangle"; "Names"; "Suffix"] (OptionSet(Some(next ())))
+
     |"-profile-ltac-cutoff" ->
       let oval = add_set_option oval ["Ltac"; "Profiling"] (OptionSet None) in
       add_set_option oval ["Ltac"; "Profiling"; "Cutoff"] (OptionSet (Some (next ())))

test-suite/failure/name_mangling_ssr.v

@@ -0,0 +1,12 @@
+Set Mangle Names.
+Set Mangle Names Light.
+Set Mangle Names Prefix "‗".
+Set Mangle Names Suffix "‗".
+
+
+Require Import ssreflect.
+Goal forall (H:True), True.
+Proof.
+  intro.
+  Fail exact ‗H‗.
+Admitted.

test-suite/success/name_mangling_ssr.v

@@ -0,0 +1,10 @@
+Set Mangle Names.
+Set Mangle Names Light.
+Set Mangle Names Prefix "‗".
+Set Mangle Names Suffix "‗".
+
+Goal forall (H:True), True.
+Proof.
+  intro.
+  exact ‗H‗.
+Qed.