diff options
| author | Lasse Blaauwbroek | 2020-12-18 09:38:34 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-12-18 09:38:34 +0100 |
| commit | a84ff9806f0ee77e081954453ee6afb67921eb50 (patch) | |
| tree | 419cff5c75b26095421226d75616026834100002 /plugins | |
| parent | 1c400a19aeb70842453f83a26f5abafc59901242 (diff) | |
Make ssr datastructures cpattern and rpattern public
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 17b47227cb..1573998f6f 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -22,15 +22,9 @@ open Genintern (** The type of context patterns, the patterns of the [set] tactic and [:] tactical. These are patterns that identify a precise subterm. *) -type cpattern +type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option val pr_cpattern : cpattern -> Pp.t -(** The type of rewrite patterns, the patterns of the [rewrite] tactic. - These patterns also include patterns that identify all the subterms - of a context (i.e. "in" prefix) *) -type rpattern -val pr_rpattern : rpattern -> Pp.t - (** Pattern interpretation and matching *) exception NoMatch @@ -48,6 +42,12 @@ type ('ident, 'term) ssrpattern = type pattern = evar_map * (constr, constr) ssrpattern val pp_pattern : env -> pattern -> Pp.t +(** The type of rewrite patterns, the patterns of the [rewrite] tactic. + These patterns also include patterns that identify all the subterms + of a context (i.e. "in" prefix) *) +type rpattern = (cpattern, cpattern) ssrpattern +val pr_rpattern : rpattern -> Pp.t + (** Extracts the redex and applies to it the substitution part of the pattern. @raise Anomaly if called on [In_T] or [In_X_In_T] *) val redex_of_pattern : |