diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 14:53:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 14:53:53 +0200 |
| commit | cd38c2030bbe024ce3c47d50d8cd961905263d43 (patch) | |
| tree | 55ab85ee98fd844ed2029711474239f3838e5c5b /pretyping/detyping.ml | |
| parent | 723b1cbb1a3b0933abf5a78a2fbcdd7bdfc5cc23 (diff) | |
| parent | 5436ca063dd8a1ae22f2b70bd8f69277c64a0624 (diff) | |
Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42 style is ugly
Diffstat (limited to 'pretyping/detyping.ml')
| -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 69a49749c..f3e8e72bb 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) |