diff options
| author | Pierre-Marie Pédrot | 2020-05-13 14:01:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-13 16:59:46 +0200 |
| commit | f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 (patch) | |
| tree | 39f979c1f1808034e6bdc15daff247a01d359c0a /engine/univMinim.mli | |
| parent | d80458841316ca7edf7317ef412142e27133c931 (diff) | |
Make explicit that UGraph lower bounds are only of two kinds.
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
Diffstat (limited to 'engine/univMinim.mli')
| -rw-r--r-- | engine/univMinim.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/univMinim.mli b/engine/univMinim.mli index 2a46d87609..58853e47b8 100644 --- a/engine/univMinim.mli +++ b/engine/univMinim.mli @@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t) (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t -> +val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> |