diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 01:33:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 01:33:53 +0200 |
| commit | e372f0e5f0646eb4209baa06c874b4f041ed6574 (patch) | |
| tree | 0eb3b9bc736d4e5cdcd022b315cf7c2a4f0731a0 /plugins/ssrmatching/g_ssrmatching.mli | |
| parent | d47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff) | |
| parent | a9728d5a43e5c82fed9cac25e841107c4c95fc35 (diff) | |
Merge PR #7898: Remove camlp4 remains
Diffstat (limited to 'plugins/ssrmatching/g_ssrmatching.mli')
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli index bb5161a0e..588a1a3ea 100644 --- a/plugins/ssrmatching/g_ssrmatching.mli +++ b/plugins/ssrmatching/g_ssrmatching.mli @@ -5,13 +5,13 @@ open Genarg open Ssrmatching (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) -val cpattern : cpattern Pcoq.Gram.entry +val cpattern : cpattern Pcoq.Entry.t val wit_cpattern : cpattern uniform_genarg_type (** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) -val lcpattern : cpattern Pcoq.Gram.entry +val lcpattern : cpattern Pcoq.Entry.t val wit_lcpattern : cpattern uniform_genarg_type (** 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 +val rpattern : rpattern Pcoq.Entry.t val wit_rpattern : rpattern uniform_genarg_type |