aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-21 17:06:37 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-21 17:54:37 +0200
commit95400806e85aaea109740e8fa77c0edb9f8b7a09 (patch)
treef61cc56a27fb3e9f210618129787eabf2af1f88e /pretyping
parent7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff)
A possible fix to BZ#5750 (ability to print context of ltac subterm match).
The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1".
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/detyping.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 1eb22cdb8..f61638db8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -460,8 +460,11 @@ and detype_r d flags avoid env sigma t =
in GVar (Id.of_string s))
| Meta n ->
(* Meta in constr are not user-parsable and are mapped to Evar *)
- (* using numbers to be unparsable *)
- GEvar (Id.of_string ("M" ^ string_of_int n), [])
+ if n = Constr_matching.special_meta then
+ (* Using a dash to be unparsable *)
+ GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
+ else
+ 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)