4 files changed, 58 insertions, 24 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.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
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 191a4e9a20..d083d34b52 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -596,26 +596,6 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF
           Ssrview.AdaptorDb.declare k hints }
 END
 
-(** Canonical Structure alias *)
-
-GRAMMAR EXTEND Gram
-  GLOBAL: gallina_ext;
-
-  gallina_ext:
-      (* Canonical structure *)
-     [[ IDENT "Canonical"; qid = Constr.global ->
-          { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) }
-      | IDENT "Canonical"; ntn = Prim.by_notation ->
-          { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) }
-      | IDENT "Canonical"; qid = Constr.global;
-          d = G_vernac.def_body ->
-          { let s = coerce_reference_to_id qid in
-    Vernacexpr.VernacDefinition
-      ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
-          ((CAst.make (Name s)),None), d) }
-  ]];
-END
-
 (** Keyword compatibility fixes. *)
 
 (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *)