Merge branch 'v8.5' into v8.6

1 files changed, 7 insertions, 0 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index bc68f11ff0..fae75f8254 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -409,6 +409,9 @@ module Unsafe : sig
   (** Like {!tclEVARS} but also checks whether goals have been solved. *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
+  (** Set the global environment of the tactic *)
+  val tclSETENV : Environ.env -> unit tactic
+
   (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
       being proved, appending them to the list of focused goals. If a
       goal is already solved, it is not added. *)
@@ -518,6 +521,10 @@ module Goal : sig
       FIXME: encapsulate the level in an existential type. *)
   val goals : ([ `LZ ], 'r) t tactic list tactic
 
+  (** [unsolved g] is [true] if [g] is still unsolved in the current
+      proof state. *)
+  val unsolved : ('a, 'r) t -> bool tactic
+
   (** Compatibility: avoid if possible *)
   val goal : ([ `NF ], 'r) t -> Evar.t