AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disque

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

3 files changed, 15 insertions, 25 deletions

diff --git a/tactics/AutoRewrite.v b/tactics/AutoRewrite.v
index 531f4ee91..2810f4cc5 100644
--- a/tactics/AutoRewrite.v
+++ b/tactics/AutoRewrite.v
@@ -7,7 +7,8 @@ Grammar vernac orient : ast :=
 
 with vernac : ast :=
 | hint_rew_b [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
-  identarg($b) "."] -> [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b) ]
+  identarg($b) "."] ->
+  [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC (Idtac))) ]
 | hint_rew_t [ "Hint" "Rewrite" orient($o) "[" ne_constrarg_list($l) "]" "in"
   identarg($b) "using" tacarg($t) "." ] ->
   [ (HintRewrite $o (CONSTRLIST ($LIST $l)) $b (TACTIC $t)) ].
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 921280f3c..f57b3f32c 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -12,9 +12,12 @@ open Term
 open Util
 open Vernacinterp
 
+(* Rewriting rules *)
+type rew_rule = constr * bool * tactic
+
 (* Summary and Object declaration *)
 let rewtab =
-  ref ((Hashtbl.create 53):(string,constr * bool * tactic) Hashtbl.t)
+  ref ((Hashtbl.create 53) : (string,rew_rule) Hashtbl.t)
 
 let lookup id = Hashtbl.find id !rewtab
 
@@ -28,8 +31,8 @@ let _ =
       Summary.init_function     = init;
       Summary.survive_section   = false }
 
-(* Rewriting rules *)
-type rew_rule = constr * bool * tactic
+(* Rewriting rules before tactic interpretation *)
+type raw_rew_rule = constr * bool * t
 
 (* Applies all the rules of one base *)
 let one_base tac_main bas =
@@ -53,7 +56,8 @@ let autorewrite tac_main lbas =
 (* Functions necessary to the library object declaration *)
 let load_hintrewrite _ = ()
 let cache_hintrewrite (_,(rbase,lrl)) =
-  List.iter (fun c -> Hashtbl.add !rewtab rbase c) lrl
+  List.iter
+    (fun (c,b,t) -> Hashtbl.add !rewtab rbase (c,b,Tacinterp.interp t)) lrl
 let export_hintrewrite x = Some x
 
 (* Declaration of the Hint Rewrite library object *)
@@ -72,19 +76,6 @@ let add_rew_rules base lrul =
 (* The vernac declaration of HintRewrite *)
 let _ = vinterp_add "HintRewrite"
   (function
-    | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id]
-      when ort = "LR" || ort = "RL" ->
-      (fun () ->
-       let (evc,env) = Command.get_current_context () in
-       let lcsr =
-         List.map (function
-	   | Node(loc,"CONSTR",l) ->
-             constr_of_Constr (interp_tacarg
-             (evc,env,[],[],None,Tactic_debug.DebugOff)
-             (Node(loc,"COMMAND",l)))
-           | _ -> bad_vernac_args "HintRewrite") lcom in
-       add_rew_rules (string_of_id id)
-         (List.map (fun csr -> (csr,ort = "LR",tclIDTAC)) lcsr))
     | [VARG_STRING ort;VARG_CONSTRLIST lcom;VARG_IDENTIFIER id;VARG_TACTIC t]
       when ort = "LR" || ort = "RL" ->
       (fun () ->
@@ -95,10 +86,9 @@ let _ = vinterp_add "HintRewrite"
              constr_of_Constr (interp_tacarg
              (evc,env,[],[],None,Tactic_debug.DebugOff)
              (Node(loc,"COMMAND",l)))
-           | _ -> bad_vernac_args "HintRewrite") lcom
-       and tac = Tacinterp.interp t in
+           | _ -> bad_vernac_args "HintRewrite") lcom in
        add_rew_rules (string_of_id id)
-         (List.map (fun csr -> (csr,ort = "LR",tac)) lcsr))
+         (List.map (fun csr -> (csr,ort = "LR",t)) lcsr))
     | _  -> bad_vernac_args "HintRewrite")
 
 (* To get back the tactic arguments and call AutoRewrite *)
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 9215eced3..2e291e542 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -2,13 +2,12 @@
 (*i $Id$ i*)
 
 open Tacmach
-open Term
 
-(* Rewriting rules *)
-type rew_rule = constr * bool * tactic
+(* Rewriting rules before tactic interpretation *)
+type raw_rew_rule = Term.constr * bool * Coqast.t
 
 (* To add rewriting rules to a base *)
-val add_rew_rules : string -> rew_rule list -> unit
+val add_rew_rules : string -> raw_rew_rule list -> unit
 
 (* The AutoRewrite tactic *)
 val autorewrite : tactic -> string list -> tactic