From fa48ee84a1829816c9e7e46f1b5172f83e8cc954 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 4 Dec 2014 09:00:37 +0100
Subject: Factoring 2ee213b824dda48c3fe60e95316daf09f07e8075.

I can't say I condone having unsafe primitives which are not used anywhere. But if they are to be there, let's make sure they don't duplicate code.---
 proofs/proofview.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 1813c716eb..f5087b2c9a 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -802,15 +802,9 @@ 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 tclGETGOALS = Comb.get
 
-  let tclSETGOALS gls =
-    Pv.modify begin fun step ->
-      let gls = undefined step.solution gls in
-      { step with comb = gls }
-    end
+  let tclSETGOALS = Comb.set
 
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
-- 
cgit v1.2.3