aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml2
1 files changed, 1 insertions, 1 deletions
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;