diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 458714403a..cc9b840bed 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -147,7 +147,7 @@ let interp_cstrs env (sigma, ind_rel) impls params ind arity = let interp_cstr sigma ctyp = let flags = Pretyping.{ all_no_fail_flags with - use_typeclasses = false; + use_typeclasses = UseTCForConv; solve_unification_constraints = false } in let sigma, (ctyp, cimpl) = interp_type_evars_impls ~flags env sigma ~impls ctyp in |