diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-21 17:08:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-21 17:54:38 +0200 |
| commit | dc5b8f1793c6f7104f0b4762d9887be255709ead (patch) | |
| tree | f30002a972f425295b98df3098686a0946091480 /pretyping/detyping.ml | |
| parent | 95400806e85aaea109740e8fa77c0edb9f8b7a09 (diff) | |
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?
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 f61638db8..5e1430741 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) |