diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-02 23:48:23 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-02 23:57:22 +0200 |
commit | a0e47bcf277d11ec7d2272bc5167fee898ad9016 (patch) | |
tree | e4323e150457f947400cd26c84ef294f33c1da97 /kernel/univ.mli | |
parent | 0c320e79ba30bf567d4ca194bc114d733baf76e5 (diff) |
Implement module subtyping for polymorphic constants (errors on
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
Diffstat (limited to 'kernel/univ.mli')
-rw-r--r-- | kernel/univ.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 7c0c9536f..296868836 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -273,6 +273,9 @@ sig val equal : t -> t -> bool (** Equality *) + val length : t -> int + (** Instance length *) + val hcons : t -> t (** Hash-consing. *) @@ -318,6 +321,8 @@ sig val instance : t -> Instance.t val constraints : t -> constraints + val dest : t -> Instance.t * constraints + (** Keeps the order of the instances *) val union : t -> t -> t |