diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index c3b9bde9b8..0961edb6cb 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -243,7 +243,9 @@ let interp_refine ist gl rc = Pretyping.use_typeclasses = true; solve_unification_constraints = true; fail_evar = false; - expand_evars = true } + expand_evars = true; + program_mode = false; + } in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) |