From fa9c33e37ca609981aca88d6f92b07882bd2f4f4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Apr 2016 16:05:15 +0200
Subject: Removing redundant *_TYPED AS clauses in EXTEND statements.

---
 ltac/extraargs.ml4 | 17 -----------------
 1 file changed, 17 deletions(-)

(limited to 'ltac/extraargs.ml4')

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 4d3507cbc4..f2dc024c71 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 =
-- 
cgit v1.2.3


From d632f64403da813e240973a9caf06c79e262a7ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Apr 2016 16:41:49 +0200
Subject: Adding toplevel representation sharing for some generic arguments.

---
 ltac/extraargs.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'ltac/extraargs.ml4')

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index f2dc024c71..fbae17bafc 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -104,6 +104,7 @@ let glob_occs ist l = l
 let subst_occs evm l = l
 
 ARGUMENT EXTEND occurrences
+  TYPED AS int list
   PRINTED BY pr_int_list_full
 
   INTERPRETED BY interp_occs
@@ -152,6 +153,7 @@ ARGUMENT EXTEND lconstr
 END
 
 ARGUMENT EXTEND lglob
+  TYPED AS glob
     PRINTED BY pr_globc
 
      INTERPRETED BY interp_glob
-- 
cgit v1.2.3