diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 18:58:16 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 09:55:10 +0100 |
| commit | c9f3a6cbe5c410256fe88580019f5c7183bab097 (patch) | |
| tree | 766ec5d728e14080066fec43b99a6928198629c3 /kernel/univ.mli | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
Fix #6677: Critical bug with VM and universes
This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 63bef1b81..f550872ba 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -125,6 +125,13 @@ sig val for_all : (Level.t * int -> bool) -> t -> bool val map : (Level.t * int -> 'a) -> t -> 'a list + + (** [compact u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] + *) + val compact : t -> t * int list end type universe = Universe.t |