Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.

4 files changed, 24 insertions, 9 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
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 6243e5e68..694ecfa37 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -13,4 +13,4 @@ open Proofview
 
 val apply_top_tac : unit tactic
 
-val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic
+val inner_ssrapplytac : ssrterm list -> ssrterm ssragens -> ist -> unit tactic
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index b8716c0c4..89cba4be7 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -29,11 +29,11 @@ val tclIPATssr : ssripats -> unit Proofview.tactic
      [tac E: gens => ipats]
    where [E] is injected into [ipats] (at the right place) and [gens] are
    generalized before calling [tac] *)
-val ssrmovetac : ssrmovearg -> unit Proofview.tactic
+val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic
 val ssrsmovetac : unit Proofview.tactic
-val ssrelimtac : ssrmovearg -> unit Proofview.tactic
+val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic
 val ssrselimtoptac : unit Proofview.tactic
-val ssrcasetac : ssrmovearg -> unit Proofview.tactic
+val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic
 val ssrscasetoptac : unit Proofview.tactic
 
 (* The implementation of abstract: is half here, for the [[: var ]]
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