From 5129c5b02bcab1426636d18583ec7a4a46195f0a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 2 Jan 2016 16:55:03 +0100
Subject: Reduce dependencies of interface files.

---
 pretyping/nativenorm.mli | 1 -
 pretyping/patternops.mli | 1 -
 pretyping/vnorm.mli      | 1 -
 3 files changed, 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 0352038385..286cb2e079 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 0148280287..34191db344 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 9421b2d859..b75fe7c928 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
-- 
cgit v1.2.3