diff options
Diffstat (limited to 'vernac/vernacextend.mli')
| -rw-r--r-- | vernac/vernacextend.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 6189830929..46cee30a1e 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -71,7 +71,7 @@ type vernac_classification = vernac_type * vernac_when (** Interpretation of extended vernac phrases. *) -type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.t option -> Proof_global.t option +type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.stack option -> Proof_global.stack option type plugin_args = Genarg.raw_generic_argument list |