aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r--pretyping/termops.ml2
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 ".")