aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/nativenorm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/nativenorm.mli')
-rw-r--r--pretyping/nativenorm.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index bbda55f48..0b1ce8e51 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -8,7 +8,6 @@
open Term
open Environ
open Evd
-open Nativelambda
(** This module implements normalization by evaluation to OCaml code *)