ExtraRedExpr maintenant sans argument: pas très souple mais au moins convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 13 insertions, 18 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8274092187..c578c66b3c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -185,7 +185,7 @@ GEXTEND Gram
       | IDENT "Fold"; cl = LIST1 constr -> Fold cl
       | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl
       | IDENT "Vm_compute" -> CbvVm   
-      | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+      | s = IDENT; OPT constr -> ExtraRedExpr s ] ]
   ;
   hypident:
     [ [ id = id_or_meta -> id,[],(InHyp,ref None)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index dfb90f610d..49dd4fa309 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -218,7 +218,7 @@ GEXTEND Gram
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
-      | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+      | s = IDENT -> ExtraRedExpr s ] ]
   ;
   hypident:
     [ [ id = id_or_meta -> id,(InHyp,ref None)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index c76de59f14..c3d865c0e4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -370,8 +370,7 @@ let pr_red_expr (pr_constr,pr_ref) = function
   | Fold l -> hov 1 (str "Fold" ++ prlist (pr_arg pr_constr) l)
   | Pattern l -> hov 1 (str "Pattern " ++ prlist (pr_occurrences pr_constr) l)
   | Red true -> error "Shouldn't be accessible from user"
-  | ExtraRedExpr (s,c) ->
-      hov 1 (str s ++ pr_arg pr_constr c)
+  | ExtraRedExpr s -> str s
   | CbvVm -> str "vm_compute" 
 
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a7c4a12af6..37dcc22b19 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -257,9 +257,8 @@ let mlexpr_of_red_expr = function
       let f = mlexpr_of_list mlexpr_of_occ_constr in
       <:expr< Rawterm.Pattern $f l$ >>
   | Rawterm.CbvVm -> <:expr< Rawterm.CbvVm >>
-  | Rawterm.ExtraRedExpr (s,c) ->
-      let l = mlexpr_of_constr c in
-      <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ $l$ >>
+  | Rawterm.ExtraRedExpr s ->
+      <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
   | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >>
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 48b41444eb..054312ff34 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -350,7 +350,7 @@ type ('a,'b) red_expr_gen =
   | Unfold of 'b occurrences list
   | Fold of 'a list
   | Pattern of 'a occurrences list
-  | ExtraRedExpr of string * 'a
+  | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 0a582ef7bb..127eb1dc6d 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -123,7 +123,7 @@ type ('a,'b) red_expr_gen =
   | Unfold of 'b occurrences list
   | Fold of 'a list
   | Pattern of 'a occurrences list
-  | ExtraRedExpr of string * 'a
+  | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9f5dec3f34..cae0705c05 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -876,7 +876,7 @@ let reduction_of_redexp = function
   | Unfold ubinds -> unfoldn ubinds
   | Fold cl -> fold_commands cl
   | Pattern lp -> pattern_occs lp
-  | ExtraRedExpr (s,c) ->
+  | ExtraRedExpr s ->
       (try Stringmap.find s !red_expr_tab
       with Not_found -> error("unknown user-defined reduction \""^s^"\""))
   | CbvVm -> cbv_vm 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 33d375dffe..a4360e5ea6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -553,8 +553,8 @@ let intern_redexp ist = function
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
   | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
-  | (Red _ | Hnf | CbvVm as r ) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c)
+  | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
+  
 
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
@@ -1235,8 +1235,7 @@ let redexp_interp ist sigma env = function
   | Lazy f -> Lazy (interp_flag ist env f)
   | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
   | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
-  | (Red _ |  Hnf | CbvVm as r) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c)
+  | (Red _ |  Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
 
@@ -1894,8 +1893,7 @@ let subst_redexp subst = function
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
   | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
-  | (Red _ | Hnf | CbvVm as r) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c)
+  | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
   | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c)
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 9057730eec..846b6468c3 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -780,8 +780,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
         pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l)
         
   | Red true -> error "Shouldn't be accessible from user"
-  | ExtraRedExpr (s,c) ->
-      hov 1 (str s ++ pr_arg pr_constr c)
+  | ExtraRedExpr s -> str s
   | CbvVm -> str "vm_compute"
 
 let rec pr_may_eval test prc prlc pr2 = function