From a2549c7f716e870ea19fdbfd7b5493117fe21e76 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Dec 2018 05:50:12 +0100
Subject: [proof] Rework proof interface.

- deprecate the old 5-tuple accessor in favor of a view record,

- move `name` and `kind` proof data from `Proof_global` to `Proof`,
  this will prove useful in subsequent functionalizations of the
  interface, in particular this is what abstract, which lives in the
  monads, needs in order no to access global state.

- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
---
 tactics/hints.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index faff116af4..571ad9d160 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1516,8 +1516,8 @@ let pr_hint_term env sigma cl =
 let pr_applicable_hint () =
   let env = Global.env () in
   let pts = Proof_global.give_me_the_proof () in
-  let glss,_,_,_,sigma = Proof.proof pts in
-  match glss with
+  let Proof.{goals;sigma} = Proof.data pts in
+  match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
     pr_hint_term env sigma (Goal.V82.concl sigma g)
-- 
cgit v1.2.3