Try only using TC for conversion in cominductive (not great but let's see)

1 files changed, 1 insertions, 1 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 000b34ed0a..53254e9511 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) env sigma =
   let env = Evd.evar_filtered_env env evi in
   let sigma',typed_c =
     let flags = {
-      Pretyping.use_typeclasses = true;
+      Pretyping.use_typeclasses = Pretyping.UseTC;
       Pretyping.solve_unification_constraints = true;
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true;