diff options
| author | Maxime Dénès | 2017-11-03 10:54:11 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-03 10:54:11 +0100 |
| commit | 97e82c1a520382ec34cfedcc55b5190126b05703 (patch) | |
| tree | d3cb12a29b9d90db3063f2488cba4961b8b46c81 /pretyping/patternops.mli | |
| parent | 22c3a0edacef219206ad216b3cce2aa73d9ce2a6 (diff) | |
| parent | de7d2fdb97975dcd94005bb6fa79a312c8afa017 (diff) | |
Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous variables).
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 ffe0186af0..2d1ce1dbc9 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 |