aboutsummaryrefslogtreecommitdiff
path: root/tactics/redops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/redops.ml')
-rw-r--r--tactics/redops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/redops.ml b/tactics/redops.ml
index e0473cbefd..86ed8f8899 100644
--- a/tactics/redops.ml
+++ b/tactics/redops.ml
@@ -10,7 +10,7 @@
open Genredexpr
-let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
+let union_consts l1 l2 = Util.List.union (=) l1 l2 (* FIXME *)
let make_red_flag l =
let rec add_flag red = function