diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 15 |
1 files changed, 15 insertions, 0 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 *) |