ssrcommon: API to call resolve_tyclasses on a term

2 files changed, 24 insertions, 0 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ebe4aac213..be8f3603e4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -499,6 +499,22 @@ let pf_e_type_of gl t =
   let sigma, ty = Typing.type_of env sigma t in
   re_sig it sigma, ty
 
+let pf_resolve_typeclasses ~where ~fail gl =
+  let sigma, env, it = project gl, pf_env gl, sig_it gl in
+  let filter =
+    let evset = Evarutil.undefined_evars_of_term sigma where in
+    fun k _ -> Evar.Set.mem k evset in
+  let sigma = Typeclasses.resolve_typeclasses ~filter ~fail env sigma in
+  re_sig it sigma
+
+let resolve_typeclasses ~where ~fail env sigma =
+  let filter =
+    let evset = Evarutil.undefined_evars_of_term sigma where in
+    fun k _ -> Evar.Set.mem k evset in
+  let sigma = Typeclasses.resolve_typeclasses ~filter ~fail env sigma in
+  sigma
+
+
 let nf_evar sigma t = 
   EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))
 
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 566a933522..cf4e4b354e 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -335,6 +335,14 @@ val refine_with :
            ?beta:bool ->
            ?with_evars:bool ->
            evar_map * EConstr.t -> v82tac
+
+val pf_resolve_typeclasses :
+  where:EConstr.t ->
+  fail:bool -> Goal.goal Evd.sigma -> Goal.goal Evd.sigma
+val resolve_typeclasses :
+  where:EConstr.t ->
+  fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
+
 (*********************** Wrapped Coq  tactics *****************************)
 
 val rewritetac : ssrdir -> EConstr.t -> tactic