From f617aeef08441e83b13f839ce767b840fddbcf7d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 14 Oct 2015 10:39:55 +0200 Subject: Fix some typos. --- kernel/byterun/coq_interp.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 399fa843f..1653c3b01 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1271,7 +1271,7 @@ value coq_interprete Instruct (COMPAREINT31) { /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ - /* assumes Inudctive _ : _ := Eq | Lt | Gt */ + /* assumes Inductive _ : _ := Eq | Lt | Gt */ print_instr("COMPAREINT31"); if ((uint32_t)accu == (uint32_t)*sp) { accu = 1; /* 2*0+1 */ -- cgit v1.2.3