diff options
| author | herbelin | 2009-10-03 10:11:35 +0000 |
|---|---|---|
| committer | herbelin | 2009-10-03 10:11:35 +0000 |
| commit | 32222d67e21922966a49dccff81f99dd7ef5ec05 (patch) | |
| tree | b028dbd36847f111a0d535c00c44b6bf2dff3960 | |
| 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
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 15 | ||||
| -rw-r--r-- | toplevel/coqcompat.ml | 3 |
3 files changed, 18 insertions, 3 deletions
@@ -12,7 +12,8 @@ Tactics source of incompatibilities solvable by redefining "intuition" as "unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".) - Improved support of dependent goals over objects in dependent types for - "destruct" (rare source of incompatibility). + "destruct" (rare source of incompatibility that can be avoided by unsetting + option "Dependent Propositions Elimination"). - Tactic "quote" now supports quotation of arbitrary terms (not just the goal). - Tactic "idtac" now displays its "list" arguments. diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9ec0485736..302c84a5ea 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 diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml index 59dca330c4..b2c1ea23bc 100644 --- a/toplevel/coqcompat.ml +++ b/toplevel/coqcompat.ml @@ -21,7 +21,8 @@ let set_compat_options = function | "8.2" -> set_bool_option_value ["Tactic";"Evars";"Pattern";"Unification"] false; set_bool_option_value ["Discriminate";"Introduction"] false; - set_bool_option_value ["Intuition";"Iff";"Unfolding"] true + set_bool_option_value ["Intuition";"Iff";"Unfolding"] true; + set_bool_option_value ["Dependent";"Propositions";"Elimination"] false; | "8.1" -> warning "Compatibility with version 8.1 not supported." |