summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
Diffstat (limited to 'common')
-rw-r--r--common/Values.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/common/Values.v b/common/Values.v
index 9f73e33..1c03789 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1107,7 +1107,7 @@ Proof. unfold inject_incr. auto. Qed.
Lemma inject_incr_trans :
forall f1 f2 f3,
inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 .
-Proof .
+Proof.
unfold inject_incr; intros. eauto.
Qed.