From 4345aec5fc74ea726536c530abcb15b1df829373 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Jun 2016 22:04:24 +0200
Subject: [PATCH] Name some intro-ed stuff.

---
 algebra/frac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/frac.v b/algebra/frac.v
index 9efcba2c2..47fd97642 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -14,7 +14,7 @@ Instance frac_op : Op frac := λ x y, (x + y)%Qp.
 Definition frac_ra_mixin : RAMixin frac.
 Proof.
   split; try apply _; try done.
-  unfold valid, op, frac_op, frac_valid. intros. trans (x+y)%Qp. 2:done.
+  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
   rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
 Qed.
 Canonical Structure fracR := discreteR frac frac_ra_mixin.
-- 
GitLab