diff options
| -rw-r--r-- | pretyping/detyping.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5750.v | 3 |
2 files changed, 8 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) diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v new file mode 100644 index 000000000..6d0e21f5d --- /dev/null +++ b/test-suite/bugs/closed/5750.v @@ -0,0 +1,3 @@ +(* Check printability of the hole of the context *) +Goal 0 = 0. +match goal with |- context c [0] => idtac c end. |