diff options
| author | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 12:51:16 +0200 |
| commit | 7543449792d417a92092b692986d62b622b78ffc (patch) | |
| tree | 8244b6c3efa88abe12ab990a4ae4b3d0af8f5dc1 /intf | |
| parent | bff880ffb6ef33c99a96e7925c995b31b1497e6a (diff) | |
| parent | 9615c025a2a09b69f2001d44a66a1fddef74e680 (diff) | |
Merge remote-tracking branch 'github/pr/299' into v8.6
Was PR#299: Fix bug #4869, allow Prop, Set, and level names in
constraints.
Diffstat (limited to 'intf')
| -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 1063a74d9f..279b587831 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -347,7 +347,7 @@ type vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of (lident * Univ.constraint_type * lident) list + | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list (* Gallina extensions *) | VernacBeginSection of lident |