diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-22 11:27:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-22 11:27:12 +0200 |
| commit | 95305e675a4e21f2425f2ffa9662095d864d9083 (patch) | |
| tree | b1e7804aa956ed5684754b43d8c66243376f9240 /pretyping | |
| parent | 7c760b08d690922fd15c489dd63a7be534d765ab (diff) | |
| parent | dc5b8f1793c6f7104f0b4762d9887be255709ead (diff) | |
Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a context obtained by ltac pattern-matching)
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1eb22cdb8..5e1430741 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 ("INTERNAL#" ^ string_of_int n), []) | Var id -> (try let _ = Global.lookup_named id in GRef (VarRef id, None) with Not_found -> GVar id) |