diff options
Diffstat (limited to 'plugins/ring/Setoid_ring_theory.v')
| -rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index dd722f8011..870fe40f1c 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -406,7 +406,7 @@ Unset Implicit Arguments. Definition Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. intros until 1; case H. -split; intros; simpl in |- *; eauto. +split; intros; simpl; eauto. Defined. Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >-> |