diff options
| author | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-02 08:56:59 +0200 |
| commit | 083e83a2e82c17c13b5af7d59029d4ef0aa1b613 (patch) | |
| tree | 7609e9b92c93fe21603aaa2f7d90805e30812f53 /kernel/uGraph.mli | |
| parent | 1f74267d7e4affe14dbafc1a6f1e6f3f465f75a8 (diff) | |
| parent | 24a9a9c4bef18133c0b5070992d3396ff7596a7c (diff) | |
Merge PR #9918: Fix #9294: critical bug with template polymorphism
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot
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 e1b5868d55..d90f01d8d1 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -48,7 +48,7 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t exception AlreadyDeclared -val add_universe : Level.t -> bool -> t -> t +val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t @@ -86,7 +86,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t val domain : t -> LSet.t (** Known universes *) -val check_subtype : AUContext.t check_function +val check_subtype : lbound:Level.t -> AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) |