diff options
| author | Gaëtan Gilbert | 2020-02-27 14:06:16 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:43 +0200 |
| commit | 699152de685ba5e2dc05fd6248b17c3139987bb7 (patch) | |
| tree | 63cd99709c431fc6cb73886622bff9f22457be9e /vernac/comInductive.ml | |
| parent | f19cf4259f63a9c0392c922527e0e9002192949e (diff) | |
Try only using TC for conversion in cominductive (not great but let's see)
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 |