diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 28 |
1 files changed, 2 insertions, 26 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 27a558611e..62d344cc02 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -79,7 +79,6 @@ let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop } ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; @@ -88,7 +87,6 @@ END (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram GLOBAL: ssrtac3arg; @@ -204,17 +202,6 @@ ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi } | [ ident(id) ] -> { Id (SsrHyp(Loc.tag ~loc id)) } END -{ - -let pr_ssrhyps _ _ _ = pr_hyps - -} - -ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY { pr_ssrhyps } - INTERPRETED BY { interp_hyps } - | [ ssrhyp_list(hyps) ] -> { check_hyps_uniq [] hyps; hyps } -END - (** Rewriting direction *) { @@ -310,18 +297,13 @@ GRAMMAR EXTEND Gram END -ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl } -| [ ssrsimpl_ne(sim) ] -> { sim } -| [ ] -> { Nop } -END - { let pr_ssrclear _ _ _ = pr_clear mt } -ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyps PRINTED BY { pr_ssrclear } +ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyp list PRINTED BY { pr_ssrclear } | [ "{" ne_ssrhyp_list(clr) "}" ] -> { check_hyps_uniq [] clr; clr } END @@ -1005,7 +987,6 @@ let pr_ssrfwdidx _ _ _ = pr_ssrfwdid (* We use a primitive parser for the head identifier of forward *) (* tactis to avoid syntactic conflicts with basic Coq tactics. *) ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -1564,7 +1545,6 @@ let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) = ARGUMENT EXTEND ssrdoarg TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses) PRINTED BY { pr_ssrdoarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -1587,7 +1567,7 @@ let pr_ssrseqarg env sigma _ _ prt = function (* an unindexed tactic. *) ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option)) PRINTED BY { pr_ssrseqarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } + END { @@ -1867,7 +1847,6 @@ let pr_ssrseqdir _ _ _ = function } ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END TACTIC EXTEND ssrtclseq @@ -2004,7 +1983,6 @@ let pr_ssreqid _ _ _ = pr_eqid (* We must use primitive parsing here to avoid conflicts with the *) (* basic move, case, and elim tactics. *) ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY { pr_ssreqid } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -2326,7 +2304,6 @@ let noruleterm loc = mk_term xNoFlag (mkCProp loc) } ARGUMENT EXTEND ssrrule_ne TYPED AS (ssrrwkind * ssrterm) PRINTED BY { pr_ssrrule } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END GRAMMAR EXTEND Gram @@ -2413,7 +2390,6 @@ let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs } ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { |