From 8c6dfd9330d5a89c1f8cc295142ff0c36384457a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 21 Sep 2006 15:10:08 +0000
Subject: Visibilité des Rewrite Hint dès le chargement du module, sans
 nécessiter sans ouverture, comme c'est le cas pour les autres Hints

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9157 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/autorewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d513653f5b..eb8e07173d 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -209,8 +209,8 @@ 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.load_function = (fun _ -> cache_hintrewrite);
        Libobject.subst_function = subst_hintrewrite;
        Libobject.classify_function = classify_hintrewrite;
        Libobject.export_function = export_hintrewrite }
-- 
cgit v1.2.3