diff options
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 9483f0220..1588856f7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -391,7 +391,7 @@ let rec detype (isgoal:bool) avoid env t = in GVar (dl, Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) - GEvar (dl, n, None) + GEvar (dl, Evar.unsafe_of_int n, None) | Var id -> (try let _ = Global.lookup_named id in GRef (dl, VarRef id) with Not_found -> GVar (dl, id)) |