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

---
 plugins/funind/indfun_common.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7b0d7d27d7..c6f5c27458 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -508,7 +508,6 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
 let decompose_lam_n sigma n =
-  let open EConstr in
   if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 plugins/funind/indfun_common.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6f5c27458..848b44a603 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -21,12 +21,9 @@ let get_name avoid ?(default="H") = function
   | Name n -> Name n
 
 let array_get_start a =
-  try
-    Array.init
-      (Array.length a - 1)
-      (fun i -> a.(i))
-  with Invalid_argument "index out of bounds" ->
-    invalid_arg "array_get_start"
+  Array.init
+    (Array.length a - 1)
+    (fun i -> a.(i))
 
 let id_of_name = function
     Name id -> id
-- 
cgit v1.2.3