From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 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 5b42add285..429e5005ec 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -459,7 +459,6 @@ let extract_mrectype sigma t =
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let open EConstr in
   let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
   match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
-- 
cgit v1.2.3