aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-02 15:45:17 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-10-02 15:47:09 +0200
commitb46020a6ea52d77b49a12e6891575b3516b8d766 (patch)
treebf1fe9bc6d70ac44111f755dca30ed3c4d90b286 /toplevel/command.mli
parentd02c9c566c58e566a1453827038f2b49b695c0a5 (diff)
parentdecdd5b3cc322936f7d1e7cc3bb363a2957d404e (diff)
Merge branch 'v8.6'
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} *)