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 ++--
 tactics/leminv.ml | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

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)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index caf4c1eca3..356b43ec14 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
    scheme on sort [sort]. Depending on the value of [dep_option] it will
    build a dependent lemma or a non-dependent one *)
 
-let inversion_scheme env sigma t sort dep_option inv_op =
+let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
     try find_rectype env sigma i
@@ -201,7 +201,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     user_err ~hdr:"lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
+  let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
@@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       invEnv ~init:Context.Named.empty
   end in
   let avoid = ref Id.Set.empty in
-  let _,_,_,_,sigma = Proof.proof pf in
+  let Proof.{sigma} = Proof.data pf in
   let sigma = Evd.minimize_universes sigma in
   let rec fill_holes c =
     match EConstr.kind sigma c with
@@ -236,7 +236,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   p, sigma
 
 let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
-  let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+  let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
   let univs =
     Evd.const_univ_entry ~poly sigma
   in
-- 
cgit v1.2.3