From 95400806e85aaea109740e8fa77c0edb9f8b7a09 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Sep 2017 17:06:37 +0200
Subject: A possible fix to BZ#5750 (ability to print context of ltac subterm
 match).

The main fix is to use is_ident_soft. The rest of the commit is to
provide something a bit more appealing than "?M-1".
---
 pretyping/detyping.ml         | 7 +++++--
 test-suite/bugs/closed/5750.v | 3 +++
 2 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/5750.v

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1eb22cdb81..f61638db81 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -460,8 +460,11 @@ and detype_r d flags avoid env sigma t =
 	 in GVar (Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
-        (* using numbers to be unparsable *)
-	GEvar (Id.of_string ("M" ^ string_of_int n), [])
+        if n = Constr_matching.special_meta then
+          (* Using a dash to be unparsable *)
+	  GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
+        else
+	  GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (VarRef id, None)
 	 with Not_found -> GVar id)
diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v
new file mode 100644
index 0000000000..6d0e21f5d0
--- /dev/null
+++ b/test-suite/bugs/closed/5750.v
@@ -0,0 +1,3 @@
+(* Check printability of the hole of the context *)
+Goal 0 = 0.
+match goal with |- context c [0] => idtac c end.
-- 
cgit v1.2.3


From dc5b8f1793c6f7104f0b4762d9887be255709ead Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Sep 2017 17:08:59 +0200
Subject: Proposing meta names more distinguishable from evar names than ?M42.

Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability.

Tough maybe it signals too much an unelegant debugging flavor?
---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f61638db81..5e14307418 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -464,7 +464,7 @@ and detype_r d flags avoid env sigma t =
           (* Using a dash to be unparsable *)
 	  GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
         else
-	  GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
+	  GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), [])
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (VarRef id, None)
 	 with Not_found -> GVar id)
-- 
cgit v1.2.3