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/ssrparser.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/ssrparser.mli')
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index a52248614..130550388 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -20,3 +20,16 @@ val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type +(* Parsing witnesses, needed to serialize ssreflect syntax *) +open Ssrmatching_plugin +open Ssrmatching +open Ssrast +open Ssrequality + +val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type +val wit_ssrclauses : clauses Genarg.uniform_genarg_type +val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type +val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type +val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type +val wit_ssrhavefwdwbinders : + (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type |