aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:55:03 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-01-02 16:55:03 +0100
commit5129c5b02bcab1426636d18583ec7a4a46195f0a (patch)
tree4451c458340f449eaffe2195e01e16d55431370a /pretyping
parent82ac0604888679bc2fbdeda9ac264d7cd10f7928 (diff)
Reduce dependencies of interface files.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/nativenorm.mli1
-rw-r--r--pretyping/patternops.mli1
-rw-r--r--pretyping/vnorm.mli1
3 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 035203838..286cb2e07 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 *)
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 014828028..34191db34 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Context
open Term
open Globnames
open Glob_term
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 9421b2d85..b75fe7c92 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -8,7 +8,6 @@
open Term
open Environ
-open Evd
(** {6 Reduction functions } *)
val cbv_vm : env -> constr -> types -> constr