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)

---
 proofs/evar_refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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