aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/evar_refiner.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 000b34ed0a..53254e9511 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) env sigma =
let env = Evd.evar_filtered_env env evi in
let sigma',typed_c =
let flags = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;