Opacify the type of hint metadata.

1 files changed, 14 insertions, 1 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9595fa2033..78ed81ec37 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1576,4 +1576,17 @@ let run_hint tac k = match warn_hint () with
     let info = Exninfo.reify () in
     Proofview.tclZERO ~info (UserError (None, (str "Tactic failure.")))
 
-let repr_hint h = h.obj
+module FullHint =
+struct
+  type t = full_hint
+  let priority (h : t) = h.pri
+  let is_polymorphic (h : t) = h.poly
+  let pattern (h : t) = h.pat
+  let database (h : t) = h.db
+  let run (h : t) k = run_hint h.code k
+  let print env sigma (h : t) = pr_hint env sigma h.code
+  let name (h : t) = h.name
+  let secvars (h : t) = h.secvars
+
+  let repr (h : t) = h.code.obj
+end