diff options
| author | Hugo Herbelin | 2020-03-31 23:48:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-31 23:48:49 +0200 |
| commit | 04af77a6b138bb139751053d63651f7187ea9952 (patch) | |
| tree | eda57819139540b03cf1e6a5e15ec558954bb484 /proofs | |
| parent | e98e8a03cae984a10fddc8acbe8fd781d4608b24 (diff) | |
| parent | fafc731885f84656ec884d40b843aa62a5991025 (diff) | |
Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 |
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; |