aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.mli')
-rw-r--r--toplevel/command.mli2
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} *)