Make bounded variables in coq unification error messages human-readable

[thewalker77]

Description of the problem

This is not a bug, but feature request.

The error messages that coq generate when it fails to unify contains variables with really long names that are sometimes hard to keep track of. An example is something similar to this:

Unable to unify
 "P ?M1359 ?M1360 --> P ?M1359 ?M1361"
with "P t1 x -->* P t1 z".

It would be more readable if the auto-generated names were something simpler, like:

Unable to unify
 "P ?x ?y --> P ?x ?z"
with "P t1 x -->* P t1 z".

Or even using the same style of M + number but using short numbers instead of long numbers such as:

Unable to unify
  "P ?M0 ?M1 --> P ?M0 ?M2"
with "P t1 x -->* P t1 z".

I am not sure if there would be a technical issue that could prevent similar feature from being implemented, but it will certainly be helpful when doing long interactive proofs.

[herbelin]

At some time, the ?Mxxxx variable names are supposed to disappear (see #15518). Meanwhile, something simple can probably be done specifically for the error messages.

If you are familiar with compiling from source, you may try this patch, and if it works and have the mood for it, don't hesitate to try submit a PR.

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 847faae7d0..8b2259dd35 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -782,7 +782,9 @@ and detype_r d flags avoid env sigma t =
           (* Using a dash to be unparsable *)
           GEvar (CAst.make @@ Id.of_string_soft "CONTEXT-HOLE", [])
         else
-          GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), [])
+          (match Evd.meta_name sigma n with
+          | Name id -> GEvar (CAst.make id, [])
+          | Anonymous -> GEvar (CAst.make @@ Id.of_string_soft ("M" ^ string_of_int n), []))
     | Var id ->
         (* Discriminate between section variable and non-section variable *)
         (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None)

[herbelin]

A bit more care should be taken to avoid collision with non-?Mxxxx variables. Here is an example:

Goal exists n, 0*0=n.
eexists.
rewrite mult_n_Sm.
(* The message should distinguish the ?n in the goal from the ?n in the statement of `mult_n_Sm` *)

The above patch would then need to be extended.

[thewalker77]

@herbelin, I am really grateful for the patch, I am not good enough with coq to setup from source, and unfortunately I have no experience with Ocaml.

I would however hope that we can keep the issue open until the enhancement is in master.