diff options
Diffstat (limited to 'plugins/setoid_ring/newring.ml4')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 24cb84ed5..14fd9192e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -389,9 +389,7 @@ let _ = Summary.init_function = (fun () -> from_carrier := Cmap.empty; from_relation := Cmap.empty; - from_name := Spmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + from_name := Spmap.empty) } let add_entry (sp,_kn) e = (* let _ = ty e.ring_lemma1 in @@ -971,9 +969,7 @@ let _ = Summary.init_function = (fun () -> field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty; - field_from_name := Spmap.empty); - Summary.survive_module = false; - Summary.survive_section = false } + field_from_name := Spmap.empty) } let add_field_entry (sp,_kn) e = (* |