From e7707310e3138c4fc455d26d5b06f372a5760bdd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Dec 2004 23:15:03 +0000
Subject: 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
---
 pretyping/rawterm.ml  | 2 +-
 pretyping/rawterm.mli | 2 +-
 pretyping/tacred.ml   | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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 
-- 
cgit v1.2.3