aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml5
1 files changed, 1 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0d0b6158d9..444ac5ab6d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,10 +67,7 @@ let print_no_symbol = ref false
(**********************************************************************)
(* Turning notations and scopes on and off for printing *)
-module IRuleSet = Set.Make(struct
- type t = interp_rule
- let compare x y = Pervasives.compare x y
- end)
+module IRuleSet = InterpRuleSet
let inactive_notations_table =
Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)