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
---
 tactics/tacinterp.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'tactics')

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