From e28edfdc3c373af7f5ca4fbd716c8c5753494d5a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jul 2020 20:06:07 +0200
Subject: Export a dedicated function that applies immediately a hint.

---
 tactics/hints.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9fac66515a..683691d5c4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1620,3 +1620,9 @@ let connect_hint_clenv h gl =
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
+
+let hint_res_pf ?with_evars ?with_classes ?flags h =
+  Proofview.Goal.enter begin fun gl ->
+    let clenv, _ = connect_hint_clenv h gl in
+    Clenv.res_pf ?with_evars ?with_classes ?flags clenv
+  end
-- 
cgit v1.2.3