diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-24 16:13:28 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-24 16:13:28 +0000 |
| commit | 0c68df5ccdacb5d2ed50b533ad613723914dfee7 (patch) | |
| tree | c83306fc05e7f70bdcd756086368e04b32e2699b /contrib/ring | |
| parent | 7f40f2807d4046a7cea8e83cb0a983cdc6401f78 (diff) | |
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
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/Ring_theory.v | 2 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 2901942ef..c04eee57e 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 7b96983a7..d2c379659 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 |