diff options
| -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 c29c443b69..c591101241 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -684,7 +684,7 @@ let rec subst_glob_constr subst raw = | _ -> knd in let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in - if nsolve == solve && nknd = knd then raw + if nsolve == solve && nknd == knd then raw else GHole (loc, nknd, nsolve) | GCast (loc,r1,k) -> |