diff options
| -rw-r--r-- | contrib/ring/Setoid_ring_theory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index a0d587eb34..891a1bf89d 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -434,7 +434,7 @@ Implicit Arguments Off. Definition Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. -NewDestruct 1. +Intros until 1; Case H. Split; Intros; Simpl; EAuto. Defined. |