3 files changed, 15 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5ab65583a0..38f4284415 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -110,7 +110,7 @@ let functional_induction with_clean c princl pat =
 	    }
 	in
 	Tacticals.tclTHEN
-	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
+	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl )
 	  (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl)
 	  g
       else Tacticals.tclIDTAC g
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index fb1204c1f6..9c15d9d12e 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -483,9 +483,22 @@ let add_Function is_general f =
 let pr_table () = pr_table !from_function
 (*********************************)
 (* Debuging *)
+let functional_induction_rewrite_dependent_proofs = ref true
 let function_debug = ref false
 open Goptions
 
+let functional_induction_rewrite_dependent_proofs_sig = 
+  {
+    optsync = false;
+    optname = "functional induction rewrite dependent";
+    optkey =  ["functional_induction_rewrite_dependent"];
+    optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
+    optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
+  }
+let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
+
+let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
+
 let function_debug_sig =
   {
     optsync = false;
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 87d646ab89..6f6607fccc 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -111,6 +111,7 @@ val pr_table : unit -> Pp.std_ppcmds
 
 (* val function_debug : bool ref  *)
 val do_observe : unit -> bool
+val do_rewrite_dependent : unit -> bool
 
 (* To localize pb *)
 exception Building_graph of exn