diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-28 20:07:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-28 20:26:46 +0200 |
| commit | de7d2fdb97975dcd94005bb6fa79a312c8afa017 (patch) | |
| tree | d2739984aa3f2090c17b9d18f884f1986c52dff0 /pretyping/patternops.mli | |
| parent | e5659c8ffe735c530a707a61c692a3af21a79a9a (diff) | |
Fixing #5401 (printing of patterns with bound anonymous variables).
This fixes also #5731, #6035, #5364.
Diffstat (limited to 'pretyping/patternops.mli')
| -rw-r--r-- | pretyping/patternops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index ffe0186af..2d1ce1dbc 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -22,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool val subst_pattern : substitution -> constr_pattern -> constr_pattern +val noccurn_pattern : int -> constr_pattern -> bool + exception BoundPattern (** [head_pattern_bound t] extracts the head variable/constant of the |