aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacextend.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacextend.mli')
-rw-r--r--vernac/vernacextend.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index e1e3b4cfe5..070c737882 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -77,7 +77,7 @@ type typed_vernac =
| VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t)
| VtReadProofOpt of (pstate:Declare.Proof.t option -> unit)
| VtReadProof of (pstate:Declare.Proof.t -> unit)
- | VtReadProgram of (pm:Declare.OblState.t -> unit)
+ | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit)
| VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t)
| VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t)
| VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t)