Merge PR #9557: [ssreflect] Export more parsing witnesses.

2 files changed, 56 insertions, 0 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 9ce9250a43..0897d3b45b 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -137,6 +137,9 @@ type 'tac ssrhint = bool * 'tac option list
 type 'tac fwdbinders =
         bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
 
+type 'tac ffwbinders =
+  (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint))
+
 type clause =
   (ssrclear * ((ssrhyp_or_id * string) *
               Ssrmatching_plugin.Ssrmatching.cpattern option) option)
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index a2cbd3c9c8..7844050272 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -32,6 +32,19 @@ type ssrfwdview = ast_closure_term list
 type ssreqid = ssripat option
 type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats))
 
+val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type
+val wit_ssrseqarg : (Tacexpr.raw_tactic_expr ssrseqarg, Tacexpr.glob_tactic_expr ssrseqarg, Geninterp.Val.t ssrseqarg) Genarg.genarg_type
+
+val wit_ssrintrosarg :
+  (Tacexpr.raw_tactic_expr * ssripats,
+   Tacexpr.glob_tactic_expr * ssripats,
+   Geninterp.Val.t * ssripats) Genarg.genarg_type
+
+val wit_ssrsufffwd :
+  (Tacexpr.raw_tactic_expr ffwbinders,
+   Tacexpr.glob_tactic_expr ffwbinders,
+   Geninterp.Val.t ffwbinders) Genarg.genarg_type
+
 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
@@ -47,3 +60,43 @@ val wit_ssrhintarg :
   (Tacexpr.raw_tactic_expr ssrhint,
    Tacexpr.glob_tactic_expr ssrhint,
    Tacinterp.Value.t ssrhint) Genarg.genarg_type
+
+val wit_ssrexactarg : ssrapplyarg Genarg.uniform_genarg_type
+val wit_ssrcongrarg : ((int * ssrterm) * cpattern ssragens) Genarg.uniform_genarg_type
+val wit_ssrfwdid : Names.Id.t Genarg.uniform_genarg_type
+
+val wit_ssrsetfwd :
+  ((ssrfwdfmt * (cpattern * ast_closure_term option)) * ssrdocc) Genarg.uniform_genarg_type
+
+val wit_ssrdoarg :
+  (Tacexpr.raw_tactic_expr ssrdoarg,
+   Tacexpr.glob_tactic_expr ssrdoarg,
+   Tacinterp.Value.t ssrdoarg) Genarg.genarg_type
+
+val wit_ssrhint :
+  (Tacexpr.raw_tactic_expr ssrhint,
+   Tacexpr.glob_tactic_expr ssrhint,
+   Tacinterp.Value.t ssrhint) Genarg.genarg_type
+
+val wit_ssrhpats : ssrhpats Genarg.uniform_genarg_type
+val wit_ssrhpats_nobs : ssrhpats Genarg.uniform_genarg_type
+val wit_ssrhpats_wtransp : ssrhpats_wtransp Genarg.uniform_genarg_type
+
+val wit_ssrposefwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type
+
+val wit_ssrrpat : ssripat Genarg.uniform_genarg_type
+val wit_ssrterm : ssrterm Genarg.uniform_genarg_type
+val wit_ssrunlockarg : (ssrocc * ssrterm) Genarg.uniform_genarg_type
+val wit_ssrunlockargs : (ssrocc * ssrterm) list Genarg.uniform_genarg_type
+
+val wit_ssrwgen : clause Genarg.uniform_genarg_type
+val wit_ssrwlogfwd : (clause list * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type
+
+val wit_ssrfixfwd : (Names.Id.t * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type
+val wit_ssrfwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type
+val wit_ssrfwdfmt : ssrfwdfmt Genarg.uniform_genarg_type
+
+val wit_ssrcpat : ssripat Genarg.uniform_genarg_type
+val wit_ssrdgens : cpattern ssragens Genarg.uniform_genarg_type
+val wit_ssrdgens_tl : cpattern ssragens Genarg.uniform_genarg_type
+val wit_ssrdir : ssrdir Genarg.uniform_genarg_type