diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
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 |