2 files changed, 3 insertions, 3 deletions
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;