From 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 17 Jun 2014 14:26:02 +0200
Subject: Removing dead code.

---
 pretyping/retyping.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping/retyping.ml')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 53c2603d8..aa33c3286 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -16,7 +16,6 @@ open Inductiveops
 open Names
 open Reductionops
 open Environ
-open Declarations
 open Termops
 
 type retype_error =
-- 
cgit v1.2.3