From c87579a20b8f99b8dd968320f96dd470d274c3ca Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 15 Jan 2015 18:45:27 +0530
Subject: 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.

---
 kernel/reduction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 62f454047f..4153b323b6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -350,7 +350,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = Closure.oracle_of_infos infos in
          let (app1,app2) =
-           if Conv_oracle.oracle_order oracle l2r (conv_key fl1) (conv_key fl2) then
+           if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
              | Some def1 -> ((lft1, whd def1 v1), appr2)
              | None ->
-- 
cgit v1.2.3