diff options
| author | Maxime Dénès | 2017-11-23 18:08:49 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 18:08:49 +0100 |
| commit | 167c52c6a15db5e094835244aff3ba76c78b391e (patch) | |
| tree | 550a25dd9fe910868b233a66dd4dd33bca943343 /engine/uState.mli | |
| parent | 915554785ffed11370f5d700d11a8b5614408096 (diff) | |
| parent | 2db70092d63065be8a5902764e0d1d5f1ea01e6c (diff) | |
Merge PR #6203: Fix universe polymorphic Program obligations.
Diffstat (limited to 'engine/uState.mli')
| -rw-r--r-- | engine/uState.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index b31e94b285..1c906fcb2d 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -104,6 +104,11 @@ val add_global_univ : t -> Univ.Level.t -> t universe. Otherwise the variable is just made flexible. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +(** Turn all undefined flexible algebraic variables into simply flexible + ones. Can be used in case the variables might appear in universe instances + (typically for polymorphic program obligations). *) +val make_flexible_nonalgebraic : t -> t + val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t |