diff options
| author | Enrico Tassi | 2018-11-28 21:23:27 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-28 21:23:27 +0100 |
| commit | 1ca73b4ba5e16af3baed6c804d0d0eeaac9eccd5 (patch) | |
| tree | b923c55393ec399513f205852e4f9ef70b1fc59a /plugins/ssr/ssrparser.mli | |
| parent | 320f8c4503293b37c852548e4d19ff4dd1c191cb (diff) | |
| parent | 9c73e11bdcea5880501572c31d3ee66abf95299d (diff) | |
Merge PR #9070: [ssreflect] Export more parsing witnesses.
Diffstat (limited to 'plugins/ssr/ssrparser.mli')
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 862a93765d..a2cbd3c9c8 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -28,10 +28,22 @@ open Ssrmatching open Ssrast open Ssrequality +type ssrfwdview = ast_closure_term list +type ssreqid = ssripat option +type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) + +val wit_ssripatrep : ssripat Genarg.uniform_genarg_type +val wit_ssrarg : ssrarg Genarg.uniform_genarg_type 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 + (Tacexpr.raw_tactic_expr fwdbinders, + Tacexpr.glob_tactic_expr fwdbinders, + Tacinterp.Value.t fwdbinders) Genarg.genarg_type +val wit_ssrhintarg : + (Tacexpr.raw_tactic_expr ssrhint, + Tacexpr.glob_tactic_expr ssrhint, + Tacinterp.Value.t ssrhint) Genarg.genarg_type |