diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0b0ff2fb5..df3d243f1 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -737,7 +737,7 @@ let rec subst_glob_constr subst raw = | GSort _ -> raw - | GHole (loc, knd, solve) -> + | GHole (loc, knd, naming, solve) -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -746,7 +746,7 @@ let rec subst_glob_constr subst raw = in let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw - else GHole (loc, nknd, nsolve) + else GHole (loc, nknd, naming, nsolve) | GCast (loc,r1,k) -> let r1' = subst_glob_constr subst r1 in |