From d236c7362053c4fc8f1c7f3b59248b412b029fb8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 21 Jun 2018 18:02:40 +0200
Subject: Define and use UGraph.enforce_leq_alg for subtyping inference

Not sure if worth using in other places.
---
 kernel/uGraph.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e6dd629e4..8c2d877b0 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -42,6 +42,9 @@ val merge_constraints : Constraint.t -> t -> t
 val check_constraint  : t -> univ_constraint -> bool
 val check_constraints : Constraint.t -> t -> bool
 
+(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *)
+val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
+
 (** Adds a universe to the graph, ensuring it is >= or > Set.
    @raise AlreadyDeclared if the level is already declared in the graph. *)
 
-- 
cgit v1.2.3