diff options
| author | Arnaud Spiwack | 2014-12-04 09:00:37 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-12-04 14:38:05 +0100 |
| commit | fa48ee84a1829816c9e7e46f1b5172f83e8cc954 (patch) | |
| tree | 9ebba478647a704e9dc28fccabf7e8c6a24d44df | |
| parent | 9fc63bfa8c8e8bc3bf835ebb2d3d444c5a6d4f9f (diff) | |
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.
| -rw-r--r-- | proofs/proofview.ml | 10 |
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 }) |