diff options
| author | Gaëtan Gilbert | 2019-05-20 17:08:38 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (patch) | |
| tree | 9bf108186e892513ac4a949a3b6ddf31c05ef328 /vernac/vernacextend.ml | |
| parent | 788b47d9dd70dc9f8057d4a9353ed24f091ea917 (diff) | |
Rename Proof_global.{t -> stack}
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 008d3d854f..644413cbb9 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -53,7 +53,7 @@ type vernac_when = | VtLater type vernac_classification = vernac_type * vernac_when -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 |