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

4 files changed, 12 insertions, 12 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..7b1aa7a07a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
 
 let with_delayed_uconstr ist c tac =
   let flags = {
-    Pretyping.use_typeclasses = false;
+    Pretyping.use_typeclasses = Pretyping.NoUseTC;
     solve_unification_constraints = true;
     fail_evar = false;
     expand_evars = true;
@@ -345,7 +345,7 @@ open EConstr
 open Vars
 
 let constr_flags () = {
-  Pretyping.use_typeclasses = true;
+  Pretyping.use_typeclasses = Pretyping.UseTC;
   Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
 
 TACTIC EXTEND refine
 | [ "refine" uconstr(c) ] ->
-   { refine_tac ist false true c }
+   { refine_tac ist false Pretyping.UseTC c }
 END
 
 TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] ->
-   { refine_tac ist true true c }
+   { refine_tac ist true Pretyping.UseTC c }
 END
 
 TACTIC EXTEND notcs_refine
 | [ "notypeclasses" "refine" uconstr(c) ] ->
-   { refine_tac ist false false c }
+   { refine_tac ist false Pretyping.NoUseTC c }
 END
 
 TACTIC EXTEND notcs_simple_refine
 | [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
-   { refine_tac ist true false c }
+   { refine_tac ist true Pretyping.NoUseTC c }
 END
 
 (* Solve unification constraints using heuristics or fail if any remain *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
 
 let eval_uconstrs ist cs =
   let flags = {
-    Pretyping.use_typeclasses = false;
+    Pretyping.use_typeclasses = Pretyping.NoUseTC;
     solve_unification_constraints = true;
     fail_evar = false;
     expand_evars = true;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..b0e26e1def 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   (evd,c)
 
 let constr_flags () = {
-  use_typeclasses = true;
+  use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = true;
   expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
 let interp_type = interp_constr_gen IsType
 
 let open_constr_use_classes_flags () = {
-  use_typeclasses = true;
+  use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
 }
 
 let open_constr_no_classes_flags () = {
-  use_typeclasses = false;
+  use_typeclasses = NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
 }
 
 let pure_open_constr_flags = {
-  use_typeclasses = false;
+  use_typeclasses = NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = false;
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;