aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.ml')
-rw-r--r--library/impargs.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index 66900ee42..61ea7a87a 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -352,8 +352,9 @@ let set_manual_implicits env flags enriching autoimps l =
| (Name id,imp)::imps ->
let l',imp,m =
try
- let (b, fi, fo) = List.assoc (ExplByName id) l in
- List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi))
+ let eq = (Pervasives.(=) : explicitation -> explicitation -> bool) in (* FIXME *)
+ let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in
+ List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi))
with Not_found ->
try
let (id, (b, fi, fo)), l' = assoc_by_pos k l in