aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/dune (renamed from plugins/ssr/plugin_base.dune)2
-rw-r--r--plugins/ssr/ssrcommon.ml2
2 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/dune
index a13524bb52..a117d09a16 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/dune
@@ -5,3 +5,5 @@
(modules_without_implementation ssrast)
(flags :standard -open Gramlib)
(libraries coq.plugins.ssrmatching))
+
+(coq.pp (modules ssrvernac ssrparser))
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;