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

2 files changed, 21 insertions, 3 deletions

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index b48030b963..c9221ef758 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -576,6 +576,8 @@ END
 
 {
 
+type ssrfwdview = ast_closure_term list
+
 let pr_ssrfwdview _ _ _ = pr_view2
 
 }
@@ -637,6 +639,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
   | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v)
   | IPatTac _ -> assert false (*internal usage only *)
 
+type ssripatrep = ssripat
 let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
 
 let pr_ssripat _ _ _ = pr_ipat
@@ -1933,6 +1936,7 @@ END
 (* argument *)
 
 {
+type ssreqid = ssripatrep option
 
 let pr_eqid = function Some pat -> str " " ++ pr_ipat pat | None -> mt ()
 let pr_ssreqid _ _ _ = pr_eqid
@@ -1987,10 +1991,12 @@ END
 (* the entry point parses only non-empty arguments to avoid conflicts  *)
 (* with the basic Coq tactics.                                         *)
 
-(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *)
-
 {
 
+type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats))
+
+(* type ssrarg = ssrbwdview * (ssreqid * (ssrdgens * ssripats)) *)
+
 let pr_ssrarg _ _ _ (view, (eqid, (dgens, ipats))) =
   let pri = pr_intros (gens_sep dgens) in
   pr_view2 view ++ pr_eqid eqid ++ pr_dgens pr_gen dgens ++ pri ipats
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