From d06ab253ae62b24030fb6dd9ee949191710e8c6f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 24 May 2018 16:49:18 +0100
Subject: Revert "Allow instantiation of type or order type variables without
 kind declaration"

This reverts commit 895f868cd537277ba61dfc427fee0e288af7e226.

These are actually treated as Ints (although you could pretend they
weren't and it mostly worked).
---
 src/type_check.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index d58f38d4..f6717ea4 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1835,12 +1835,10 @@ let is_nat_kid kid = function
 
 let is_order_kid kid = function
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0
-  | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let is_typ_kid kid = function
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0
-  | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let rec instantiate_quants quants kid uvar = match quants with
-- 
cgit v1.2.3