diff options
| author | Matthieu Sozeau | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:43 +0530 |
| commit | c87579a20b8f99b8dd968320f96dd470d274c3ca (patch) | |
| tree | c0600c17af66feaee7529b6291f62b975dfc600a /kernel/reduction.ml | |
| 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/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |