diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-23 15:34:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-23 15:40:54 +0200 |
| commit | 5436ca063dd8a1ae22f2b70bd8f69277c64a0624 (patch) | |
| tree | 8595b239bdd1d6955fbef653d94157474f9390ad /pretyping/detyping.ml | |
| parent | 06a723190858da8ed3f30736f22398aa7822c959 (diff) | |
After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.
Printing metas still happens relatively often. From the user point of
view, no need to know that it is different from an evar, so the
notation ?M42 as it was before is much lighter. As for developers
looking for debugging information, they will easily suspect that it is
internally a meta because of the "M".
This reverts "Proposing meta names more distinguishable from evar
names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
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 5e1430741..f61638db8 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) |