Merge branch 'v8.5' into v8.6

1 files changed, 6 insertions, 0 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index a2838a2de1..f2f4005151 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -929,6 +929,8 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclSETENV = Env.set
+
   let tclGETGOALS = Comb.get
 
   let tclSETGOALS = Comb.set
@@ -1129,6 +1131,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self