From 777f0ace3d2458cbe1840dcf3d8f350452721e84 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 2 Feb 2015 09:30:53 +0100
Subject: Removing dead code.

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

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 654f914b61..adf714db35 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,7 +18,6 @@ open Declarations
 open Declareops
 open Environ
 open Reductionops
-open Inductive
 
 (* The following three functions are similar to the ones defined in
    Inductive, but they expect an env *)
-- 
cgit v1.2.3