From 910a8b080f1ee548a7df24245d2d46e5c3a2f9cc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Apr 2011 11:57:32 +0000
Subject: Fixing and completing interpretation of let's in notations for
 iterated binders. (backport from trunk)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14061 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 336be31d89..c2d14f8acd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2704,8 +2704,8 @@ let guess_elim isrec hyp0 gl =
   let elimc =
     if isrec then lookup_eliminator mind s
     else
-      if use_dependent_propositions_elimination () &&
-	dependent_no_evar (mkVar hyp0) (pf_concl gl)
+      if true (*use_dependent_propositions_elimination () &&
+	dependent_no_evar (mkVar hyp0) (pf_concl gl)*)
       then
 	pf_apply build_case_analysis_scheme gl mind true s
       else
-- 
cgit v1.2.3