diff options
| author | Matthieu Sozeau | 2016-09-29 15:51:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-09-29 15:56:10 +0200 |
| commit | 9615c025a2a09b69f2001d44a66a1fddef74e680 (patch) | |
| tree | 4643d4f0f38b89402265df46c56119e28a8afe40 /intf | |
| parent | 5348a615a484e379896deac8a6944af1f92b2d4c (diff) | |
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 ed44704df4..e6599a30d1 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -346,7 +346,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 |