diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 46cf163bf..05b7619e5 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 = |