diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:51:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:51:16 +0200 |
| commit | 7543449792d417a92092b692986d62b622b78ffc (patch) | |
| tree | 8244b6c3efa88abe12ab990a4ae4b3d0af8f5dc1 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/command.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index d35372429..616afb91f 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -22,7 +22,7 @@ open Pfedit val do_universe : polymorphic -> Id.t Loc.located list -> unit val do_constraint : polymorphic -> - (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit + (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit (** {6 Hooks for Pcoq} *) |