diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dfd92f0c17..8898e5989a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -717,6 +717,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_judgment_tcc evdref env c = let j = pretype empty_tycon env evdref ([],[]) c in + evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env !evdref; j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must |