From 9c6487ba87f448daa28158c6e916e3d932c50645 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 20 Oct 2004 13:50:08 +0000
Subject: COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 46cf163bf0..05b7619e52 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -20,6 +20,9 @@ open Reduction
 open Inductive
 open Type_errors
 
+let conv = vm_conv CONV
+let conv_leq = vm_conv CUMUL
+let conv_leq_vecti = vm_conv_leq_vecti
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
-- 
cgit v1.2.3