diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 7a774cc9..411ccc0e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *) +(* $Id: equality.ml 13874 2011-03-05 16:41:53Z herbelin $ *) open Pp open Util @@ -888,8 +888,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = with | Some w -> let w_type = type_of env sigma w in - if Evarconv.e_conv env evdref w_type a then - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + if Evarconv.e_cumul env evdref w_type a then + applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." | None -> anomaly "Not enough components to build the dependent tuple" |