diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-18 00:16:43 +0530 |
| commit | c87579a20b8f99b8dd968320f96dd470d274c3ca (patch) | |
| tree | c0600c17af66feaee7529b6291f62b975dfc600a /kernel/names.mli | |
| parent | 93628d2e7156943edf3cfffa25a21855fb4b06db (diff) | |
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 9fbe7d5e5..d82043da1 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -458,11 +458,8 @@ type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) -type id_key = Constant.t tableKey - val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool val eq_constant_key : Constant.t -> Constant.t -> bool -val eq_id_key : id_key -> id_key -> bool (** equalities on constant and inductive names (for the checker) *) |