diff options
| author | Hugo Herbelin | 2020-09-05 15:42:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-17 16:19:39 +0100 |
| commit | 2823c88d1dc1aa27e93217d5d3ad2e30155cd948 (patch) | |
| tree | 824c54000aca5e4792c7d9f231710c0087c3949d /interp/notation_ops.mli | |
| parent | 213207a1612d311f2f60d7e498ebd53a13ce039b (diff) | |
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
Diffstat (limited to 'interp/notation_ops.mli')
| -rw-r--r-- | interp/notation_ops.mli | 5 |
1 files changed, 5 insertions, 0 deletions
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 : |