From eb03700129e7ed7f011174f0fb10cba7c858cbb5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Apr 2011 13:05:27 +0000
Subject: Fixing commit r14061 (changes in file tactics.ml were mistakenly
 committed).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14067 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 c2d14f8acd..336be31d89 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 true (*use_dependent_propositions_elimination () &&
-	dependent_no_evar (mkVar hyp0) (pf_concl gl)*)
+      if 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