diff options
| author | Raphaël Monat | 2017-10-03 16:20:46 +0200 |
|---|---|---|
| committer | Raphaël Monat | 2017-10-03 16:20:46 +0200 |
| commit | e664022ba1314d866e4e148d5f5f925654db0487 (patch) | |
| tree | 0cb2ce6b8d3b4f735d4b2f15f2fd775bfdcd1e61 /pretyping | |
| parent | dfa56fb57b09296cdf311ec5972d2d33b787e48c (diff) | |
| parent | 2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff) | |
Merge branch 'master' of https://github.com/coq/coq
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 69a49749cd..f3e8e72bb7 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 ("INTERNAL#" ^ string_of_int n), []) + 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) |