From 9a5f2464e780a0c2aeefa8e1dc6dfc1f65d392b0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 3 Jan 2009 14:35:25 +0000
Subject: Fixed two problems: - Function descend_in_conjunctions was now too
 weak, use match_with_record. - Added documentation of new notation for
 destruct with equation.

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

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 79498076b2..c4b5803345 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -709,7 +709,7 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 let descend_in_conjunctions with_evars tac exit c gl =
   try
     let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-    match match_with_conjunction ((strip_prod t)) with
+    match match_with_record ((strip_prod t)) with
     | Some _ ->
 	let n = (mis_constr_nargs mind).(0) in
 	let sort = elimination_sort_of_goal gl in
-- 
cgit v1.2.3