From 32222d67e21922966a49dccff81f99dd7ef5ec05 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 3 Oct 2009 10:11:35 +0000
Subject: 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
---
 CHANGES               |  3 ++-
 tactics/tactics.ml    | 15 ++++++++++++++-
 toplevel/coqcompat.ml |  3 ++-
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index ecf61370d5..a65195e15c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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."
-- 
cgit v1.2.3