From ea9a239eefacf85338c1f0ca0d3dc144c7e7f20e Mon Sep 17 00:00:00 2001 From: jforest Date: Wed, 16 Dec 2009 16:03:38 +0000 Subject: adding an option functional_induction_rewrite_dependent to make functional induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/indfun_common.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'plugins/funind/indfun_common.ml') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index fb1204c1f..9c15d9d12 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; -- cgit v1.2.3