From 551b958cae1134d4f76c7e22abf42b8c2a1b97f7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Nov 2006 13:17:28 +0000
Subject: Dépendance inutile en Tacexpr, de proofs, qui se compile en principe
 après

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9392 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/clenv.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index d86f03e94e..8b1c6dfc5c 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -21,7 +21,6 @@ open Reduction
 open Reductionops
 open Rawterm
 open Pattern
-open Tacexpr
 open Tacred
 open Pretype_errors
 open Evarutil
-- 
cgit v1.2.3