diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:33 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:33 +0000 |
commit | bb5e6d7c39211349d460db0b61b2caf3d099d5b6 (patch) | |
tree | e14b120edc5fedcb1a0a114218d1cdaa0f887ed4 /pretyping/termops.ml | |
parent | 4e20ed9e5c1608226f0d736df10bb82fc402e7a2 (diff) |
cList: a few alternative to hashtbl-based uniquize, distinct, subset
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2e2389f09..899def8c8 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -696,7 +696,7 @@ let replace_term = replace_term_gen eq_constr except the ones in l *) let error_invalid_occurrence l = - let l = List.uniquize (List.sort Pervasives.compare l) in + let l = List.sort_uniquize Int.compare l in errorlabstrm "" (str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") ++ prlist_with_sep spc int l ++ str ".") |