diff options
| author | herbelin | 2004-10-13 17:26:06 +0000 |
|---|---|---|
| committer | herbelin | 2004-10-13 17:26:06 +0000 |
| commit | 2ba2a1b56b1cc2ec8b8ea63e8bd081773aab0580 (patch) | |
| tree | 6f5e0d22213d757d6b51b763e40de463f2a1484a | |
| parent | 0096dfc44e1c7db55cc28c402172f1d2ad522bf3 (diff) | |
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
| -rw-r--r-- | tactics/autorewrite.ml | 9 |
1 files 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 |