diff options
| -rw-r--r-- | ltac/extraargs.ml4 | 17 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | ltac/g_auto.ml4 | 2 | ||||
| -rw-r--r-- | ltac/g_rewrite.ml4 | 6 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 1 |
5 files changed, 0 insertions, 28 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 4d3507cbc..f2dc024c7 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -110,10 +110,7 @@ ARGUMENT EXTEND occurrences GLOBALIZED BY glob_occs SUBSTITUTED BY subst_occs - RAW_TYPED AS occurrences_or_var RAW_PRINTED BY pr_occurrences - - GLOB_TYPED AS occurrences_or_var GLOB_PRINTED BY pr_occurrences | [ ne_integer_list(l) ] -> [ ArgArg l ] @@ -141,10 +138,7 @@ ARGUMENT EXTEND glob GLOBALIZED BY glob_glob SUBSTITUTED BY subst_glob - RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - - GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ constr(c) ] -> [ c ] END @@ -164,10 +158,7 @@ ARGUMENT EXTEND lglob GLOBALIZED BY glob_glob SUBSTITUTED BY subst_glob - RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - - GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ lconstr(c) ] -> [ c ] END @@ -207,9 +198,7 @@ ARGUMENT EXTEND hloc INTERPRETED BY interp_place GLOBALIZED BY intern_place SUBSTITUTED BY subst_place - RAW_TYPED AS loc_place RAW_PRINTED BY pr_loc_place - GLOB_TYPED AS loc_place GLOB_PRINTED BY pr_loc_place [ ] -> [ ConclLocation () ] @@ -224,12 +213,6 @@ ARGUMENT EXTEND hloc END - - - - - - (* Julien: Mise en commun des differentes version de replace with in by *) let pr_by_arg_tac _prc _prlc prtac opt_c = diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index ba9f82fb9..0b475340e 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -980,9 +980,7 @@ let interp_test ist gls = function ARGUMENT EXTEND test PRINTED BY pr_itest' INTERPRETED BY interp_test - RAW_TYPED AS test RAW_PRINTED BY pr_test' - GLOB_TYPED AS test GLOB_PRINTED BY pr_test' | [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ] END diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index bc98b7d6d..d4fd8a1df 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -174,7 +174,6 @@ END let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom ARGUMENT EXTEND hints_path_atom - TYPED AS hints_path_atom PRINTED BY pr_hints_path_atom | [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] | [ "*" ] -> [ Hints.PathAny ] @@ -183,7 +182,6 @@ END let pr_hints_path prc prx pry c = Hints.pp_hints_path c ARGUMENT EXTEND hints_path - TYPED AS hints_path PRINTED BY pr_hints_path | [ "(" hints_path(p) ")" ] -> [ p ] | [ "!" hints_path(p) ] -> [ Hints.PathStar p ] diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index c4ef1f297..395c2cd1b 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -47,10 +47,7 @@ ARGUMENT EXTEND glob_constr_with_bindings GLOBALIZED BY glob_glob_constr_with_bindings SUBSTITUTED BY subst_glob_constr_with_bindings - RAW_TYPED AS constr_expr_with_bindings RAW_PRINTED BY pr_constr_expr_with_bindings - - GLOB_TYPED AS glob_constr_with_bindings GLOB_PRINTED BY pr_glob_constr_with_bindings [ constr_with_bindings(bl) ] -> [ bl ] @@ -76,10 +73,7 @@ ARGUMENT EXTEND rewstrategy GLOBALIZED BY glob_strategy SUBSTITUTED BY subst_strategy - RAW_TYPED AS raw_strategy RAW_PRINTED BY pr_raw_strategy - - GLOB_TYPED AS glob_strategy GLOB_PRINTED BY pr_glob_strategy [ glob(c) ] -> [ StratConstr (c, true) ] diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 7bd07f625..ca4e13e12 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -35,7 +35,6 @@ let pr_int_or_id _ _ _ = function | ArgId id -> pr_id id ARGUMENT EXTEND int_or_id - TYPED AS int_or_id PRINTED BY pr_int_or_id | [ preident(id) ] -> [ ArgId (Id.of_string id) ] | [ integer(i) ] -> [ ArgInt i ] |