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)

---
 user-contrib/Ltac2/tac2core.ml    | 4 ++--
 user-contrib/Ltac2/tac2tactics.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 2ed854c9f7..72df4d75c8 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -20,7 +20,7 @@ open Proofview.Notations
 let constr_flags =
   let open Pretyping in
   {
-    use_typeclasses = true;
+    use_typeclasses = Pretyping.UseTC;
     solve_unification_constraints = true;
     fail_evar = true;
     expand_evars = true;
@@ -31,7 +31,7 @@ let constr_flags =
 let open_constr_no_classes_flags =
   let open Pretyping in
   {
-  use_typeclasses = false;
+  use_typeclasses = Pretyping.NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 30ee1a0b4c..9ca38d64df 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -20,7 +20,7 @@ let return = Proofview.tclUNIT
 let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()
 
 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