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-15 18:59:00 +0530 |
| commit | 8309a98096facfba448c9d8d298ba3903145831a (patch) | |
| tree | 38a09851cb687921193b4368a93eed34ccd55a58 /kernel/vm.mli | |
| parent | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (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/vm.mli')
| -rw-r--r-- | kernel/vm.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli index fa88418ce..295ea83c4 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -24,9 +24,9 @@ type vswitch type arguments type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive + | Aid of Vars.id_key + | Aiddef of Vars.id_key * values + | Aind of pinductive (** Zippers *) @@ -54,7 +54,7 @@ type whd = val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values -val val_of_constant : constant -> values +val val_of_constant : pconstant -> values external val_of_annot_switch : annot_switch -> values = "%identity" |