From aeb20a17562fde5c07bd398da589d721e8c0aabf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 7 Oct 2014 11:23:01 +0200
Subject: Avoid a warning with Meta's names in debugger.

---
 pretyping/detyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index df3d243f1..205c5a208 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -413,7 +413,7 @@ let rec detype flags avoid env sigma t =
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
         (* using numbers to be unparsable *)
-	GEvar (dl, Id.of_string (string_of_int n), [])
+	GEvar (dl, Id.of_string ("M" ^ string_of_int n), [])
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
-- 
cgit v1.2.3