diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-08 18:06:55 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:36:30 +0200 |
| commit | 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac (patch) | |
| tree | b6b33c6c6167656b1ca9799407eeb56aa1de749f /pretyping/nativenorm.mli | |
| parent | d08aa6b4f742a7162e726920810765258802c176 (diff) | |
Fix #4346 1/2: native casts were not inferring universe constraints.
Diffstat (limited to 'pretyping/nativenorm.mli')
| -rw-r--r-- | pretyping/nativenorm.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index c854e8c9c..035203838 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -12,6 +12,8 @@ open Nativelambda (** This module implements normalization by evaluation to OCaml code *) -val evars_of_evar_map : evar_map -> evars +val native_norm : env -> evar_map -> constr -> types -> constr -val native_norm : env -> evars -> constr -> types -> constr +(** Conversion with inference of universe constraints *) +val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> + evar_map * bool |