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 60697c1611..22e67357cd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -381,7 +381,7 @@ val tclENV : Environ.env tactic
(** {7 Put-like primitives} *)
(** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Safe_typing.private_constants -> unit tactic
+val tclEFFECTS : Evd.side_effects -> unit tactic
(** [mark_as_unsafe] declares the current tactic is unsafe. *)
val mark_as_unsafe : unit tactic