diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-07 11:23:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-07 14:44:27 +0200 |
| commit | aeb20a17562fde5c07bd398da589d721e8c0aabf (patch) | |
| tree | 90dbf79e78d68d6674dd93e26fcbb21a2f2d2d78 /pretyping | |
| parent | d6851cb4ee7d351159f0e3706574b8e384e10650 (diff) | |
Avoid a warning with Meta's names in debugger.
Diffstat (limited to 'pretyping')
| -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 df3d243f1..205c5a208 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -413,7 +413,7 @@ let rec detype flags avoid env sigma t = | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) (* using numbers to be unparsable *) - GEvar (dl, Id.of_string (string_of_int n), []) + GEvar (dl, Id.of_string ("M" ^ string_of_int n), []) | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) with Not_found -> GVar (dl, id)) |