1 files changed, 6 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 3964692b10..b76c802dfd 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -433,6 +433,12 @@ let tclSENSITIVE s =
     fun env -> { go = fun sk fk step -> sk () fk (sensitive_on_step s env step) }
   end
 
+
+(*** Commands ***)
+
+let in_proofview p k =
+  k p.solution
+
 module Notations = struct
   let (>-) = Goal.bind
   let (>>-) = tclGOALBINDU