diff options
Diffstat (limited to 'pretyping/nativenorm.mli')
| -rw-r--r-- | pretyping/nativenorm.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index ecc3489be..a589846b9 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -9,7 +9,11 @@ open Names open Term open Environ open Reduction +open Evd +open Nativelambda (** This module implements normalization by evaluation to OCaml code *) -val native_norm : env -> constr -> types -> constr +val evars_of_evar_map : evar_map -> evars + +val native_norm : env -> evars -> constr -> types -> constr |