From 2823c88d1dc1aa27e93217d5d3ad2e30155cd948 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Sep 2020 15:42:32 +0200
Subject: For printing, ordering notations by precision of the pattern.

This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion
---
 interp/notation_ops.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 3cc6f82ec8..3182ea96d7 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -16,6 +16,11 @@ open Glob_term
 
 val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
 
+val strictly_finer_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
+(** Tell if [t1] is a strict refinement of [t2]
+    (this is a partial order and returning [false] does not mean that
+    [t2] is finer than [t1]) *)
+
 (** Substitution of kernel names in interpretation data                *)
 
 val subst_interpretation :
-- 
cgit v1.2.3