aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacextend.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacextend.ml')
-rw-r--r--vernac/vernacextend.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 7317818730..496b1a43d1 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -63,6 +63,7 @@ type typed_vernac =
| VtReadProgram of (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)
type vernac_command = atts:Attributes.vernac_flags -> typed_vernac