aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacextend.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacextend.ml')
-rw-r--r--vernac/vernacextend.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ed63332861..f320b65954 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -59,7 +59,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)