diff options
Diffstat (limited to 'pretyping/patternops.mli')
| -rw-r--r-- | pretyping/patternops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 3a1faf1c77..2d1ce1dbc9 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -12,6 +12,7 @@ open Glob_term open Mod_subst open Misctypes open Pattern +open Ltac_pretype (** {5 Functions on patterns} *) @@ -21,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 |