1 files 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 })