aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/proofview.mli')
-rw-r--r--engine/proofview.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 29425b10f2..8853013a84 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -474,7 +474,7 @@ module Unsafe : sig
val tclEVARUNIVCONTEXT : UState.t -> unit tactic
(** Clears the future goals store in the proof view. *)
- val reset_future_goals : proofview -> proofview
+ val push_future_goals : proofview -> proofview
(** Give the evars the status of a goal (changes their source location
and makes them unresolvable for type classes. *)