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, 2 insertions, 2 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 8b1e49919..0ebff440a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -594,7 +594,7 @@ let dispatch =
   let int31_op n op prim kn =
     { empty_reactive_info with
       vm_compiling = Some (Cbytegen.op_compilation n op kn);
-      native_compiling = Some (Nativelambda.compile_prim prim kn);
+      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
     }
   in
 
@@ -602,7 +602,7 @@ fun rk value field ->
   (* subfunction which shortens the (very common) dispatch of operations *)
   let int31_op_from_const n op prim =
     match kind_of_term value with
-      | Const (kn,_) ->  int31_op n op prim kn
+      | Const kn ->  int31_op n op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
   let int31_binop_from_const op prim = int31_op_from_const 2 op prim in