From 2ba2a1b56b1cc2ec8b8ea63e8bd081773aab0580 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 13 Oct 2004 17:26:06 +0000
Subject: Compatibilité de Hint Rewrite avec Write State

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/autorewrite.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 7c134b89b5..833941a0af 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -22,7 +22,7 @@ open Vernacinterp
 open Tacexpr
 
 (* Rewriting rules *)
-type rew_rule = constr * bool * tactic
+type rew_rule = constr * bool * glob_tactic_expr
 
 (* Summary and Object declaration *)
 let rewtab =
@@ -39,7 +39,6 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section   = false }
 
-(* Rewriting rules before tactic interpretation *)
 type raw_rew_rule = constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
@@ -51,6 +50,7 @@ let one_base tac_main bas =
       errorlabstrm "AutoRewrite" 
         (str ("Rewriting base "^(bas)^" does not exist"))
   in
+  let lrul = List.map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
         (tclREPEAT_MAIN 
@@ -65,12 +65,11 @@ let autorewrite tac_main lbas =
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  let l = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrl in
   let l = 
     try 
-      List.rev_append l (Stringmap.find rbase !rewtab) 
+      List.rev_append lrl (Stringmap.find rbase !rewtab) 
     with
-      | Not_found -> List.rev l
+      | Not_found -> List.rev lrl
   in
     rewtab:=Stringmap.add rbase l !rewtab
 
-- 
cgit v1.2.3