aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacinterp.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacinterp.mli')
-rw-r--r--vernac/vernacinterp.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index e3e708e87d..675dfd11f3 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -15,7 +15,7 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
proof and won't be forced *)
val interp_qed_delayed_proof
: proof:Declare.proof_object
- -> info:Lemmas.Info.t
+ -> info:Declare.Info.t
-> st:Vernacstate.t
-> control:Vernacexpr.control_flag list
-> Vernacexpr.proof_end CAst.t