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.

1 files changed, 7 insertions, 6 deletions

diff --git a/kernel/vm.ml b/kernel/vm.ml
index a7e5a55c45..2cc1efe431 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -137,10 +137,11 @@ type vswitch = {
 (* Generally the first field is a code pointer.                           *)
 
 (* Do not edit this type without editing C code, especially "coq_values.h" *)
+
 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 *)
 
@@ -306,11 +307,11 @@ let val_of_atom a = val_of_obj (obj_of_atom a)
 
 module IdKeyHash =
 struct
-  type t = id_key
-  let equal = Names.eq_id_key
+  type t = pconstant tableKey
+  let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal)
   open Hashset.Combine
   let hash = function
-  | ConstKey c -> combinesmall 1 (Constant.hash c)
+  | ConstKey (c,u) -> combinesmall 1 (Constant.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
 end