diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 857f75ed6..ed6ded8e1 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -448,7 +448,7 @@ type vernac_type = | VtStm of vernac_control * vernac_part_of_script | VtUnknown and vernac_qed_type = VtKeep | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list +and vernac_start = string * opacity_guarantee * Id.t list * polymorphic and vernac_sideff_type = Id.t list and vernac_is_alias = bool and vernac_part_of_script = bool |