diff options
author | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-16 16:03:38 +0000 |
---|---|---|
committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-16 16:03:38 +0000 |
commit | ea9a239eefacf85338c1f0ca0d3dc144c7e7f20e (patch) | |
tree | 461e73186eda24e2155bb13ecc09782b181cd771 /plugins/funind/indfun_common.ml | |
parent | 3f6db8c182cc45272f1b9988db687bcdd0009ab1 (diff) |
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
Diffstat (limited to 'plugins/funind/indfun_common.ml')
-rw-r--r-- | plugins/funind/indfun_common.ml | 13 |
1 files changed, 13 insertions, 0 deletions
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; |