4 files changed, 61 insertions, 5 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/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c3b9bde9b8..0961edb6cb 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -243,7 +243,9 @@ let interp_refine ist gl rc =
     Pretyping.use_typeclasses = true;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true }
+    expand_evars = true;
+    program_mode = false;
+  }
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
 (*   ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 3fb21e5ef6..2a2cd73df2 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -591,10 +591,8 @@ END
 GRAMMAR EXTEND Gram
   GLOBAL: ssrfwdview;
   ssrfwdview: [
-    [  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr ->
-            { [mk_ast_closure_term `None c] }
-    |  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview ->
-                    { (mk_ast_closure_term `None c) :: w } ]];
+    [  test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] }
+    |  test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]];
 END
 
 (* ipats *)
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