From 467eb67bb960c15e1335f375af29b4121ac5262b Mon Sep 17 00:00:00 2001
From: JPR
Date: Wed, 22 May 2019 21:40:57 +0200
Subject: Fixing typos - Part 2

---
 kernel/declarations.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 36ee952099..860d19fe26 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -22,11 +22,11 @@ type engagement = set_predicativity
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives
-    and constants hiding inductives are implicitely polymorphic when
+    and constants hiding inductives are implicitly polymorphic when
     applied to parameters, on the universes appearing in the whnf of
     their parameters and their conclusion, in a template style.
     
-    In truely universe polymorphic mode, we always use RegularArity.
+    In truly universe polymorphic mode, we always use RegularArity.
 *)
 
 type template_arity = {
-- 
cgit v1.2.3