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)

---
 plugins/ssr/ssrcommon.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 01b12474dd..e0b083a70a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -239,7 +239,7 @@ let interp_refine ist gl rc =
   } in
   let kind = Pretyping.OfType (pf_concl gl) in
   let flags = {
-    Pretyping.use_typeclasses = true;
+    Pretyping.use_typeclasses = Pretyping.UseTC;
     solve_unification_constraints = true;
     fail_evar = false;
     expand_evars = true;
-- 
cgit v1.2.3