diff options
| -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." |