From 3c9f42251c7552d4a53f93af27b3134c64a3f916 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 5 Apr 2014 14:05:26 -0400
Subject: Typo in comment.

---
 kernel/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f408de8c75..9cfa5c632e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -688,7 +688,7 @@ let get_recargs_approx env ind args =
         assert (List.is_empty largs);
 	    build_recargs (ienv_push_var ienv (na, b, mk_norec)) d
 	| Rel k ->
-        (* Free variable are allowed and assigned Norec *)
+        (* Free variables are allowed and assigned Norec *)
         (try snd (List.nth ra_env (k-1))
           with Failure _ | Invalid_argument _ -> mk_norec)
 	| Ind ind_kn ->
-- 
cgit v1.2.3