diff options
Diffstat (limited to 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 850f06f87..857f75ed6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -289,7 +289,7 @@ type vernac_expr = (* Gallina *) | VernacDefinition of (locality option * definition_object_kind) * lident * definition_expr - | VernacStartTheoremProof of theorem_kind * + | VernacStartTheoremProof of theorem_kind * (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list * bool | VernacEndProof of proof_end @@ -428,6 +428,7 @@ type vernac_expr = (* Flags *) | VernacProgram of vernac_expr + | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr and located_vernac_expr = Loc.t * vernac_expr |