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

1 files changed, 1 insertions, 1 deletions

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