aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.mli')
-rw-r--r--toplevel/command.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 163f68fd0..b12479b45 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -44,11 +44,11 @@ val interp_assumption :
val declare_assumption : coercion_flag -> assumption_kind -> types ->
manual_implicits ->
- bool (** implicit *) -> bool (* inline *) -> variable located -> unit
+ bool (** implicit *) -> inline -> variable located -> unit
val declare_assumptions : variable located list ->
coercion_flag -> assumption_kind -> types -> manual_implicits ->
- bool -> bool -> unit
+ bool -> inline -> unit
(** {6 Inductive and coinductive types} *)