diff options
author | 2014-03-01 18:26:26 +0100 | |
---|---|---|
committer | 2014-03-01 22:45:39 +0100 | |
commit | 87b510e5b0f363724eae5db9f177f167a3586015 (patch) | |
tree | 204c7ad1e1ba38945ab58d74e28d8cf67201fe71 /tactics | |
parent | bca756eaebf16b6145c65b53629219d2a0a8b1ba (diff) |
Fixing pervasive comparisons
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index d6139f529..1006fd2de 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1126,7 +1126,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let make_iterated_tuple env sigma dflt (z,zty) = let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in - let sorted_rels = List.sort Pervasives.compare (Int.Set.elements rels) in + let sorted_rels = Int.Set.elements rels in let (tuple,tuplety) = List.fold_left (make_tuple env sigma) (z,zty) sorted_rels in |