diff options
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index d198fbfbe..ba0305869 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst val ugraph : t -> UGraph.t (** The current graph extended with the local constraints *) +val initial_graph : t -> UGraph.t +(** The initial graph with just the declarations of new universes. *) + val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) |