1 files changed, 14 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c8983700f9..c478bd6635 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -838,6 +838,20 @@ module Goal = struct
     in
     tclUNIT (List.map_filter map step.comb)
 
+  let raw_goals =
+    Proof.current >>= fun env ->
+    Proof.get >>= fun step ->
+    let sigma = step.solution in
+    let map goal =
+      match Goal.advance sigma goal with
+      | None -> None (** ppedrot: Is this check really necessary? *)
+      | Some goal ->
+        (** The sigma is unchanged. *)
+        let (gl, _) = Goal.eval (raw_enter_t (fun gl -> gl)) env sigma goal in
+        Some gl
+    in
+    tclUNIT (List.map_filter map step.comb)
+
   (* compatibility *)
   let goal { self=self } = self
   let refresh_sigma g =