From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 kernel/closure.ml      | 2 +-
 kernel/fast_typeops.ml | 6 +++---
 kernel/opaqueproof.mli | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index ea9b2755f2..03e70495fb 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -771,7 +771,7 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
+(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 063c9cf126..b625478f25 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -33,7 +33,7 @@ let check_constraints cst env =
   if Environ.check_constraints cst env then ()
   else error_unsatisfied_constraints env cst
 
-(* This should be a type (a priori without intension to be an assumption) *)
+(* This should be a type (a priori without intention to be an assumption) *)
 let type_judgment env c t =
   match kind_of_term(whd_betadeltaiota env t) with
     | Sort s -> {utj_val = c; utj_type = s }
@@ -52,8 +52,8 @@ let assumption_of_judgment env t ty =
     error_assumption env (make_judge t ty)
 
 (************************************************)
-(* Incremental typing rules: builds a typing judgement given the *)
-(* judgements for the subterms. *)
+(* Incremental typing rules: builds a typing judgment given the *)
+(* judgments for the subterms. *)
 
 (*s Type of sorts *)
 
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 0609c8517e..009ff82ff5 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -11,9 +11,9 @@ open Term
 open Mod_subst
 
 (** This module implements the handling of opaque proof terms.
-    Opauqe proof terms are special since:
+    Opaque proof terms are special since:
     - they can be lazily computed and substituted
-    - they are stoked in an optionally loaded segment of .vo files
+    - they are stored in an optionally loaded segment of .vo files
     An [opaque] proof terms holds the real data until fully discharged.
     In this case it is called [direct].
     When it is [turn_indirect] the data is relocated to an opaque table
-- 
cgit v1.2.3