From 2ee213b824dda48c3fe60e95316daf09f07e8075 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Nov 2014 00:09:04 +0100
Subject: Adding missing unsafe primitives to Proofview.

---
 proofs/proofview.ml  | 10 ++++++++++
 proofs/proofview.mli |  7 +++++++
 2 files changed, 17 insertions(+)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 15110a67c9..a8b77e225f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -799,6 +799,16 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclGETGOALS =
+    let open Proof in
+    Pv.get >>= begin fun step -> tclUNIT step.comb end
+
+  let tclSETGOALS gls =
+    Pv.modify begin fun step ->
+      let gls = undefined step.solution gls in
+      { step with comb = gls }
+    end
+
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 796a6a7baa..b758559beb 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -380,6 +380,13 @@ module Unsafe : sig
       goal is already solved, it is not added. *)
   val tclNEWGOALS : Goal.goal list -> unit tactic
 
+  (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
+      goal is already solved, it is not set. *)
+  val tclSETGOALS : Goal.goal list -> unit tactic
+
+  (** [tclGETGOALS] returns the list of goals under focus. *)
+  val tclGETGOALS : Goal.goal list tactic
+
   (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
 
-- 
cgit v1.2.3