diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-11 15:14:15 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-07-27 10:10:23 +0200 |
| commit | e3c247c1d96f39d2c07d120b69598a904b7d9f19 (patch) | |
| tree | a9d3735d5d3f53140aa1123e87f4d4c8db8840f8 /plugins/ssrmatching | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
deprecate Pp.std_ppcmds type alias
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 65ea76d16..8e2a1a717 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -15,7 +15,7 @@ open Term (** The type of context patterns, the patterns of the [set] tactic and [:] tactical. These are patterns that identify a precise subterm. *) type cpattern -val pr_cpattern : cpattern -> Pp.std_ppcmds +val pr_cpattern : cpattern -> Pp.t (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) val cpattern : cpattern Pcoq.Gram.entry @@ -29,7 +29,7 @@ val wit_lcpattern : cpattern uniform_genarg_type These patterns also include patterns that identify all the subterms of a context (i.e. "in" prefix) *) type rpattern -val pr_rpattern : rpattern -> Pp.std_ppcmds +val pr_rpattern : rpattern -> Pp.t (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) val rpattern : rpattern Pcoq.Gram.entry @@ -50,7 +50,7 @@ type ('ident, 'term) ssrpattern = | E_As_X_In_T of 'term * 'ident * 'term type pattern = evar_map * (constr, constr) ssrpattern -val pp_pattern : pattern -> Pp.std_ppcmds +val pp_pattern : pattern -> 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] *) @@ -115,7 +115,7 @@ val fill_occ_pattern : the T pattern above, and calls a continuation on its occurrences. *) type ssrdir = L2R | R2L -val pr_dir_side : ssrdir -> Pp.std_ppcmds +val pr_dir_side : ssrdir -> Pp.t (** a pattern for a term with wildcards *) type tpattern @@ -225,7 +225,7 @@ val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.Id.t -> cpattern -val pr_constr_pat : constr -> Pp.std_ppcmds +val pr_constr_pat : constr -> Pp.t val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma |