AutoRewrite substitutive...

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

3 files changed, 35 insertions, 5 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ad4da1235a..c7a11846c3 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -66,11 +66,26 @@ let cache_hintrewrite (_,(rbase,lrl)) =
     (fun (c,b,t) -> Hashtbl.add !rewtab rbase (c,b,Tacinterp.interp t)) lrl
 let export_hintrewrite x = Some x
 
+let subst_hintrewrite (_,subst,(rbase,list as node)) = 
+  let subst_first (cst,b,t as pair) = 
+    let cst' = Term.subst_mps subst cst in
+      if cst == cst' then pair else
+	(cst',b,t)
+  in
+  let list' = list_smartmap subst_first list in
+    if list' == list then node else
+      (rbase,list')
+      
+let classify_hintrewrite (_,x) = Libobject.Substitute x
+
+
 (* Declaration of the Hint Rewrite library object *)
 let (in_hintrewrite,out_hintrewrite)=
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
        Libobject.open_function = (fun i o -> if i=1 then cache_hintrewrite o);
        Libobject.cache_function = cache_hintrewrite;
+       Libobject.subst_function = subst_hintrewrite;
+       Libobject.classify_function = classify_hintrewrite;
        Libobject.export_function = export_hintrewrite }
 
 (* To add rewriting rules to a base *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bec72973d6..72aa724afb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1195,7 +1195,7 @@ let substHypInConcl_RL_tac =
    SubstHypInHyp id H.
     id:a=b H:(P a) |- G
 *)
-
+(*
 (**********************************************************************)
 (*                    AutoRewrite                                     *)
 (**********************************************************************)
@@ -1232,13 +1232,28 @@ let rules_of_base rbase = List.rev (Gmapl.find rbase !rew_tab)
 
 (*Functions necessary to the library object declaration*)
 let cache_autorewrite_rule (_,(rbase,lrl)) = add_list_rules rbase lrl
+
+let subst_autorewrite_rule (_,subst,(rbase,list as node)) = 
+  let subst_first (cst,b as pair) = 
+    let cst' = Term.subst_mps subst cst in
+      if cst == cst' then pair else
+	(cst',b)
+  in
+  let list' = list_smartmap subst_first list in
+    if list' == list then node else
+      (rbase,list')
+      
+let classify_autorewrite_rule (_,x) = Libobject.Substitute x
+
 let export_autorewrite_rule x = Some x
 
 (*Declaration of the AUTOREWRITE_RULE library object*)
 let (in_autorewrite_rule,out_autorewrite_rule)=
   Libobject.declare_object {(Libobject.default_object "AUTOREWRITE_RULE") with
-       Libobject.open_function = (fun i o -> if i=1 then cache_autorewrite_rule o);
        Libobject.cache_function = cache_autorewrite_rule;
+       Libobject.open_function = (fun i o -> if i=1 then cache_autorewrite_rule o);
+       Libobject.subst_function = subst_autorewrite_rule;
+       Libobject.classify_function = classify_autorewrite_rule;
        Libobject.export_function = export_autorewrite_rule }
 
 (****The tactic****)
@@ -1497,7 +1512,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
         (fun l -> validation_gen nlvalid l)
     in
     (repackage sigr gl,validation_fun)
-
+*)
 
 (* Substitutions tactics (JCF) *)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 20ff6e4724..42b0d9b32a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -88,7 +88,7 @@ val hypSubst_LR : identifier -> clause -> tactic
 val hypSubst_RL : identifier -> clause -> tactic
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
-
+(*
 (***************)
 (* AutoRewrite *)
 (***************)
@@ -124,7 +124,7 @@ val explicit_hint_base : goal sigma -> hint_base -> rewriting_rule list
 val autorewrite :
   hint_base list -> tactic list option -> option_step 
     -> tactic list option -> bool -> int -> tactic
-
+*)
 
 (* Subst *)