From 699152de685ba5e2dc05fd6248b17c3139987bb7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Feb 2020 14:06:16 +0100
Subject: Try only using TC for conversion in cominductive (not great but let's
 see)

---
 vernac/comInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comInductive.ml')

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
-- 
cgit v1.2.3