1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 4e414b35e..6bc3a4b12 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -7,6 +7,7 @@ open Names
 open Generic
 open Term
 open Reduction
+open Inductive
 open Proof_type
 open Clenv
 open Hipattern