diff options
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 0e452621c8..8c76581478 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -3,6 +3,7 @@ open Names open Environ open Reduction open Vm +open Vmvalues open Csymtable let val_of_constr env c = @@ -93,7 +94,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let mib = Environ.lookup_mind mi env in let ulen = match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx + | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx | Declarations.Cumulative_ind cumi -> Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) @@ -204,4 +205,4 @@ let vm_conv cv_pb env t1 t2 = let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () -let _ = Reduction.set_vm_conv vm_conv +let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv |