From 0c68df5ccdacb5d2ed50b533ad613723914dfee7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 24 Nov 2000 16:13:28 +0000
Subject: certains effets disparaissent a la sortie des sections, d'autres non
 (selon Summary.survive_section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Ring_theory.v | 2 ++
 contrib/ring/ring.ml       | 3 ++-
 2 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 2901942efd..c04eee57ec 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -370,6 +370,8 @@ Save.
 
 End Theory_of_rings.
 
+Hints Resolve Th_mult_zero_left Th_plus_reg_left : core.
+
 Implicit Arguments Off.
 
 Definition Semi_Ring_Theory_of :
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 7b96983a7d..d2c379659e 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -126,7 +126,8 @@ let _ =
   Summary.declare_summary "tactic-ring-table"
     { Summary.freeze_function = (fun () -> !theories_map);
       Summary.unfreeze_function = (fun t -> theories_map := t);
-      Summary.init_function = (fun () -> theories_map := Cmap.empty) }
+      Summary.init_function = (fun () -> theories_map := Cmap.empty);
+      Summary.survive_section = false }
 
 (* declare a new type of object in the environment, "tactic-ring-theory"
    The functions theory_to_obj and obj_to_theory do the conversions
-- 
cgit v1.2.3