diff options
| author | Maxime Dénès | 2015-10-08 18:06:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-15 14:36:30 +0200 |
| commit | 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac (patch) | |
| tree | b6b33c6c6167656b1ca9799407eeb56aa1de749f /kernel/nativeconv.mli | |
| parent | d08aa6b4f742a7162e726920810765258802c176 (diff) | |
Fix #4346 1/2: native casts were not inferring universe constraints.
Diffstat (limited to 'kernel/nativeconv.mli')
| -rw-r--r-- | kernel/nativeconv.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 318a7d830b..21f0b2e9e5 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -12,3 +12,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) val native_conv : conv_pb -> evars -> types conversion_function + +(** A conversion function parametrized by a universe comparator. Used outside of + the kernel. *) +val native_conv_gen : conv_pb -> evars -> (constr, 'a) generic_conversion_function |