diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 7 |
5 files changed, 4 insertions, 11 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index fdeef5f0ac..ff106404c8 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -138,9 +138,7 @@ let warn_deprecated_syntax = ARGUMENT EXTEND firstorder_using TYPED AS reference_list PRINTED BY pr_firstorder_using_typed - RAW_TYPED AS reference_list RAW_PRINTED BY pr_firstorder_using_raw - GLOB_TYPED AS reference_list GLOB_PRINTED BY pr_firstorder_using_glob | [ "using" reference(a) ] -> [ [a] ] | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a2d31780dd..272852d47a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -48,9 +48,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option PRINTED BY pr_fun_ind_using_typed - RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using - GLOB_TYPED AS constr_with_bindings_opt GLOB_PRINTED BY pr_fun_ind_using | [ "using" constr_with_bindings(c) ] -> [ Some c ] | [ ] -> [ None ] diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index f4555509cc..0c6d10bf8c 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -285,9 +285,7 @@ let in_clause' = Pltac.in_clause ARGUMENT EXTEND in_clause TYPED AS clause_dft_concl PRINTED BY pr_in_top_clause - RAW_TYPED AS clause_dft_concl RAW_PRINTED BY pr_in_clause - GLOB_TYPED AS clause_dft_concl GLOB_PRINTED BY pr_in_clause | [ in_clause'(cl) ] -> [ cl ] END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 35ed14fc18..8eadb66edc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -62,9 +62,7 @@ let pr_auto_using _ _ _ = Pptactic.pr_auto_using ARGUMENT EXTEND auto_using TYPED AS uconstr_list PRINTED BY pr_auto_using - RAW_TYPED AS uconstr_list RAW_PRINTED BY pr_auto_using_raw - GLOB_TYPED AS uconstr_list GLOB_PRINTED BY pr_auto_using_glob | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] | [ ] -> [ [] ] diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 989a6c5bf1..d62656f95f 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -491,9 +491,10 @@ let mkhintref ?loc c n = match c.CAst.v with | _ -> mkAppC (c, mkCHoles ?loc n) ARGUMENT EXTEND ssrhintref - PRINTED BY pr_ssrhintref - RAW_TYPED AS constr RAW_PRINTED BY pr_raw_ssrhintref - GLOB_TYPED AS constr GLOB_PRINTED BY pr_glob_ssrhintref + TYPED AS constr + PRINTED BY pr_ssrhintref + RAW_PRINTED BY pr_raw_ssrhintref + GLOB_PRINTED BY pr_glob_ssrhintref | [ constr(c) ] -> [ c ] | [ constr(c) "|" natural(n) ] -> [ mkhintref ~loc c n ] END |