aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 19:03:03 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-13 19:03:03 +0100
commited0c434a05a929a659e43aed80ab7c8179a7daa3 (patch)
treed486bf54f6bbfd6ace8dc9cea52b959699f88ebe /engine/proofview.mli
parentc571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (diff)
[api] Insert miscellaneous API deprecation back to core.
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 d92d0a7d5..0379d4b49 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -426,7 +426,7 @@ module Unsafe : sig
val tclGETGOALS : Evd.evar list tactic
(** Sets the evar universe context. *)
- val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
+ val tclEVARUNIVCONTEXT : UState.t -> unit tactic
(** Clears the future goals store in the proof view. *)
val reset_future_goals : proofview -> proofview