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)

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 30ca024a2f..c79aca3d3c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1223,7 +1223,7 @@ let rec intros_move = function
    or a term with bindings *)
 
 let tactic_infer_flags with_evar = {
-  Pretyping.use_typeclasses = true;
+  Pretyping.use_typeclasses = Pretyping.UseTC;
   Pretyping.solve_unification_constraints = true;
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true;
-- 
cgit v1.2.3