diff options
| author |  Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:44:20 +0200 |
| commit | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch) | |
| tree | a418d1edb3d53cdb4185b9719b7a70822cf5a24d /tactics/equality.ml | |
| parent | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff) | |
Imported Upstream version 8.3.pl2upstream/8.3.pl2
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" |