diff options
Diffstat (limited to 'kernel/uGraph.mli')
| -rw-r--r-- | kernel/uGraph.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8a8c09e911..8d9afb0990 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -13,8 +13,8 @@ open Univ (** {6 Graphs of universes. } *) type t -val make_sprop_cumulative : t -> t -(** Don't use this in the kernel, it makes the system incomplete. *) +val set_cumulative_sprop : bool -> t -> t +(** Makes the system incomplete. *) type 'a check_function = t -> 'a -> 'a -> bool |