diff options
| author | Gaëtan Gilbert | 2020-02-27 14:06:16 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:43 +0200 |
| commit | 699152de685ba5e2dc05fd6248b17c3139987bb7 (patch) | |
| tree | 63cd99709c431fc6cb73886622bff9f22457be9e /plugins/ssr | |
| parent | f19cf4259f63a9c0392c922527e0e9002192949e (diff) | |
Try only using TC for conversion in cominductive (not great but let's see)
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 |
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; |