diff options
| author | Brian Campbell | 2018-05-24 16:49:18 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-24 16:49:18 +0100 |
| commit | d06ab253ae62b24030fb6dd9ee949191710e8c6f (patch) | |
| tree | bdbad768bf47a52abf1e9b00a4d22da0ed43b5f5 /src | |
| parent | fa2169a210a0ee911d889900d4e845629330c1de (diff) | |
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).
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 2 |
1 files changed, 0 insertions, 2 deletions
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 |