diff options
| author | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
| commit | 99cdbc25a3a92545544a087ed55240c488b42fc9 (patch) | |
| tree | 4b9f80d7ae15a421b5745dec138759a37cf68da6 /intf | |
| parent | 1c620d266885086e076011917d5b1d28af299ea1 (diff) | |
Fix bug #3289
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 3ffaca1138..be7e59a2de 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -320,7 +320,7 @@ type vernac_expr = bool * (* abstract instance *) local_binder list * (* super *) typeclass_constraint * (* instance name, class name, params *) - constr_expr option * (* props *) + (bool * constr_expr) option * (* props *) int option (* Priority *) | VernacContext of local_binder list |