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