5 files changed, 36 insertions, 5 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3a5af1dd5f..7bc5d090b4 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -366,6 +366,14 @@ let free_vars_of_constr_expr c =
     | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
   in aux [] Id.Set.empty c
 
+let names_of_constr_expr c =
+  let vars = ref Id.Set.empty in
+  let rec aux () () = function
+    | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+      let id = qualid_basename qid in vars := Id.Set.add id !vars
+    | c -> fold_constr_expr_with_binders (fun a () -> vars := Id.Set.add a !vars) aux () () c
+  in aux () () c; !vars
+
 let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 
 (* Used in correctness and interface *)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 7f14eb4583..8c735edfc9 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -119,6 +119,9 @@ val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
 val free_vars_of_constr_expr : constr_expr -> Id.Set.t
 val occur_var_constr_expr : Id.t -> constr_expr -> bool
 
+(** Return all (non-qualified) names treating binders as names *)
+val names_of_constr_expr : constr_expr -> Id.Set.t
+
 val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
 
 val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
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)
diff --git a/interp/notation.ml b/interp/notation.ml
index b0854de4a3..ca27d439fb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -50,15 +50,25 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
 | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
 
+let notation_entry_level_compare s1 s2 = match (s1,s2) with
+| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0
+| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) ->
+   pair_compare String.compare Int.compare (s1,n1) (s2,n2)
+| InConstrEntrySomeLevel, _ -> -1
+| InCustomEntryLevel _, _ -> 1
+
 let notation_eq (from1,ntn1) (from2,ntn2) =
   notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
 
 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
 
+let notation_compare =
+  pair_compare notation_entry_level_compare String.compare
+
 module NotationOrd =
   struct
     type t = notation
-    let compare = Pervasives.compare
+    let compare = notation_compare
   end
 
 module NotationSet = Set.Make(NotationOrd)
@@ -178,6 +188,17 @@ type scoped_notation_rule_core = scope_name * notation * interpretation * int op
 type notation_rule_core = interp_rule * interpretation * int option
 type notation_rule = notation_rule_core * delimiters option * bool
 
+let interp_rule_compare r1 r2 = match r1, r2 with
+  | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) ->
+      pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2)
+  | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
+  | (NotationRule _ | SynDefRule _), _ -> -1
+
+module InterpRuleSet = Set.Make(struct
+    type t = interp_rule
+    let compare = interp_rule_compare
+  end)
+
 (* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and  *)
 
 type uninterp_scope_elem =
diff --git a/interp/notation.mli b/interp/notation.mli
index 75034cad70..a482e00e81 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -210,6 +210,8 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of KerName.t
 
+module InterpRuleSet : Set.S with type elt = interp_rule
+
 val declare_notation_interpretation : notation -> scope_name option ->
       interpretation -> notation_location -> onlyprint:bool -> unit