From d741845da605f75a3cf650fe2915940ce58ddaa5 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 6 May 2015 11:26:27 +0200
Subject: Typo: Val.sun_inject -> Val.sub_inject.

---
 common/Values.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'common/Values.v')

diff --git a/common/Values.v b/common/Values.v
index a4ead481..8877f9a7 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1545,7 +1545,7 @@ Proof.
   repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
 Qed.
 
-Remark sun_inject:
+Remark sub_inject:
   forall v1 v1' v2 v2',
   inject f v1 v1' ->
   inject f v2 v2' ->
-- 
cgit