diff options
Diffstat (limited to 'plugins/ssr/ssrparser.mlg')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 10 |
1 files changed, 8 insertions, 2 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 |