From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 14 Jun 2017 16:32:47 +0200
Subject: A short cleanup

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

(limited to 'kernel')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f3b7ae2b24..21651b3e21 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -169,7 +169,7 @@ type one_inductive_body = {
     mind_reloc_tbl :  Cbytecodes.reloc_table;
   }
 
-type abstrac_inductive_universes =
+type abstract_inductive_universes =
   | Monomorphic_ind of Univ.universe_context
   | Polymorphic_ind of Univ.abstract_universe_context
   | Cumulative_ind of Univ.abstract_cumulativity_info
@@ -192,7 +192,7 @@ type mutual_inductive_body = {
 
     mind_params_ctxt : Context.Rel.t;  (** The context of parameters (includes let-in declaration) *)
 
-    mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
+    mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
-- 
cgit v1.2.3