diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-20 20:39:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-05 13:42:01 +0100 |
| commit | 0b1032f2acdb6f7d92c84ba3afcbf3818cc107a9 (patch) | |
| tree | d9ba31a2560c3f3d51db15ad22cd16bcab724357 /plugins/ssr/ssrast.mli | |
| parent | 15331729aaab16678c2f7e29dd391f72df53d76e (diff) | |
[ssreflect] Export parsing witnesses in mli file.
This is needed in order to manipulate/serialize SSR's AST.
A quicker [and maybe better] alternative would be to just remove
`ssrparser.mli`, as there are many grammar entries that still need
exporting.
Diffstat (limited to 'plugins/ssr/ssrast.mli')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 9783bc61d..7f5f2f63d 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -138,7 +138,7 @@ type ssrclseq = InGoal | InHyps type 'tac ssrhint = bool * 'tac option list type 'tac fwdbinders = - bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint)) + bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) type clause = (ssrclear * ((ssrhyp_or_id * string) * @@ -157,13 +157,15 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) open Ssrmatching_plugin open Ssrmatching + +type 'a ssrcasearg = ssripat option * ('a * ssripats) +type 'a ssrmovearg = ssrview * 'a ssrcasearg + type ssrdgens = { dgens : (ssrdocc * cpattern) list; gens : (ssrdocc * cpattern) list; clr : ssrclear } -type ssrcasearg = ssripat option * (ssrdgens * ssripats) -type ssrmovearg = ssrview * ssrcasearg -type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear -type ssrapplyarg = ssrterm list * (ssragens * ssripats) +type 'a ssragens = (ssrdocc * 'a) list list * ssrclear +type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats) (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign |