diff options
| author | herbelin | 2001-09-14 19:16:58 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-14 19:16:58 +0000 |
| commit | 34a9cfb9c008c387fae02d7f8f8c6172bfcb1798 (patch) | |
| tree | 402ff60847699cbad14bd2d46cde4128b1b9c6de | |
| parent | af731fbb7f6fb76158c1980eddcc185a7e5e630d (diff) | |
MAJ vis à vis de la nouvelle non-localité des Remark/Fact
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1971 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/Setoid_ring_normalize.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v index e49be32727..8b889b23f2 100644 --- a/contrib/ring/Setoid_ring_normalize.v +++ b/contrib/ring/Setoid_ring_normalize.v @@ -456,6 +456,10 @@ Proof. NewDestruct l;Trivial. Save. +Hint ivl_aux_ok_ := Resolve ivl_aux_ok. +Hint ics_aux_ok_ := Resolve ics_aux_ok. +Hint interp_m_ok_ := Resolve interp_m_ok. + (* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *) Lemma canonical_sum_merge_ok : (x,y:canonical_sum) |