diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-03 10:11:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-03 10:11:35 +0000 |
| commit | 32222d67e21922966a49dccff81f99dd7ef5ec05 (patch) | |
| tree | b028dbd36847f111a0d535c00c44b6bf2dff3960 /tactics | |
| parent | feb92894c6be249abadd3303cfca3b258d6f3ea8 (diff) | |
Added option "Unset Dependent Propositions Elimination" to protect
against the incompatibilities introduced by making "destruct" working
on dependent propositions (incompatibilities come from uses of
destruct in Ltac definitions such as "destruct_conjs").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12367 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9ec048573..302c84a5e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -77,6 +77,17 @@ let inj_ebindings = function let dloc = dummy_loc +(* Option for 8.2 compatibility *) +open Goptions +let dependent_propositions_elimination = ref true +let _ = + declare_bool_option + { optsync = true; + optname = "dependent-propositions-elimination tactic"; + optkey = ["Dependent";"Propositions";"Elimination"]; + optread = (fun () -> !dependent_propositions_elimination) ; + optwrite = (fun b -> dependent_propositions_elimination := b) } + (*********************************************) (* Tactics *) (*********************************************) @@ -2570,7 +2581,9 @@ let guess_elim isrec hyp0 gl = if isrec then lookup_eliminator mind s else let case = - if dependent_no_evar (mkVar hyp0) (pf_concl gl) then make_case_dep + if !dependent_propositions_elimination && + dependent_no_evar (mkVar hyp0) (pf_concl gl) + then make_case_dep else make_case_gen in pf_apply case gl mind s in let elimt = pf_type_of gl elimc in |