diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rwxr-xr-x | pretyping/classops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index c4e88f5aea..7fb1bb2ccc 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -158,7 +158,7 @@ let subst_cl_typ subst ct = match ct with | CL_FUN | CL_SECVAR _ -> ct | CL_CONST kn -> - let kn' = subst_kn subst kn in + let kn' = subst_con subst kn in if kn' == kn then ct else CL_CONST kn' | CL_IND (kn,i) -> |
